From a9abceab3e53e0dca12310e08f6cce352a0c1323 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Sun, 1 Nov 2026 15:56:19 -0500 Subject: [PATCH] refactor(crypto): migrate the remaining Crypto clients to OracleComp.sumHandler Step 3 of #814, part 2 of 2. - The remaining Crypto clients use OracleComp.sumHandler and the generic support rules OracleComp.eq_of_mem_supportWith_pure and OracleComp.mem_supportWith_map_iff. - The transitional abbreviation ProbOracleComp.handler and the support corollaries ProbOracleComp.eq_of_mem_support_pure and ProbOracleComp.mem_support_map are deleted. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- .../Crypto/Computational/CramerShoup.lean | 30 ++-- .../Computational/CramerShoup/Reductions.lean | 14 +- .../Computational/CramerShoup/Scheme.lean | 8 +- .../Encryption/EncryptThenMAC.lean | 150 +++++++++--------- .../Crypto/Computational/GGM/Expansion.lean | 18 +-- .../Crypto/Computational/GGM/Hybrid.lean | 4 +- .../Crypto/Computational/GGM/Reduction.lean | 4 +- .../Crypto/Computational/GMW/Protocol.lean | 4 +- .../Crypto/Computational/GMW/Simulator.lean | 4 +- .../Computational/IndexedSignature.lean | 4 +- .../IndexedSignature/Counter.lean | 24 +-- Complexity/Crypto/Computational/MAC.lean | 98 ++++++------ .../MerkleSignature/Security.lean | 35 ++-- .../Crypto/Computational/OneWay/MCSP.lean | 2 +- .../Computational/OneWayToSignature.lean | 10 +- .../Computational/PseudorandomFunction.lean | 14 +- .../PseudorandomFunction/Coins.lean | 24 +-- .../PseudorandomFunction/RandomOracle.lean | 10 +- .../PseudorandomFunction/TruthTable.lean | 10 +- .../Crypto/Computational/Signature.lean | 44 ++--- Complexity/Crypto/Game/UntilBad.lean | 14 +- .../Languages/Probabilistic/Oracle.lean | 7 - .../Probabilistic/Oracle/Support.lean | 10 -- 23 files changed, 262 insertions(+), 280 deletions(-) diff --git a/Complexity/Crypto/Computational/CramerShoup.lean b/Complexity/Crypto/Computational/CramerShoup.lean index 30cb50f1fa..e9709d296c 100644 --- a/Complexity/Crypto/Computational/CramerShoup.lean +++ b/Complexity/Crypto/Computational/CramerShoup.lean @@ -187,7 +187,7 @@ noncomputable def cramerShoupMsgCCA2Game let pkVal := F.cramerShoupPublicKey d α σ τ σ₁ τ₁ σ₂ τ₂ let pk := F.encodeCramerShoupPublicKeyValues d pkVal let choiceOut ← ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ()) let choice := choiceOut.1 @@ -202,7 +202,7 @@ noncomputable def cramerShoupMsgCCA2Game F.encode d (csPkH₁ pkVal), F.encode d (csPkH₂ pkVal)) m ad β.val let guessOut ← ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase2Oracle hasAD H isElem d sk ct ad)) (adversary.guess n choice.2 ct)).run ()) return guessOut.1 @@ -315,7 +315,7 @@ noncomputable def cramerShoupGame1 let w := F.encode d ((α * β) • F.generator d) let pk := F.encodeCramerShoupPublicKey d u sk let choiceOut ← ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ()) let choice := choiceOut.1 @@ -326,7 +326,7 @@ noncomputable def cramerShoupGame1 let m := if bit then m₁ else m₀ let ct := F.encodeCramerShoupChallenge H d sk v w m ad let guessOut ← ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase2Oracle hasAD H isElem d sk ct ad)) (adversary.guess n choice.2 ct)).run ()) return guessOut.1 @@ -392,7 +392,7 @@ noncomputable def cramerShoupGame2 let w := F.encode d (γ • F.generator d) let pk := F.encodeCramerShoupPublicKey d u sk let choiceOut ← ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ()) let choice := choiceOut.1 @@ -403,7 +403,7 @@ noncomputable def cramerShoupGame2 let m := if bit then m₁ else m₀ let ct := F.encodeCramerShoupChallenge H d sk v w m ad let guessOut ← ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase2Oracle hasAD H isElem d sk ct ad)) (adversary.guess n choice.2 ct)).run ()) return guessOut.1 @@ -526,7 +526,7 @@ private noncomputable def cramerShoupExactCollisionGame let w := F.encode d (γ • F.generator d) let pk := F.encodeCramerShoupPublicKey d u sk let choiceOut ← ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ()) let choice := choiceOut.1 @@ -584,7 +584,7 @@ private theorem advantage_cramerShoupGame2_game3_le_exactCollision let ct := F.encodeCramerShoupChallenge H d sk v w m ad have hrun : (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase2Oracle hasAD H isElem d sk ct ad)) (adversary.guess n choiceOut.1.2 ct)).run ())).bind (fun guessOut => PMF.pure guessOut.1) = @@ -639,7 +639,7 @@ private theorem succProbability_cramerShoupExactCollisionGame_le let w := F.encode d (γ • F.generator d) let pk := F.encodeCramerShoupPublicKey d u sk (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ())).bind fun choiceOut => let choice := choiceOut.1 @@ -666,7 +666,7 @@ private theorem succProbability_cramerShoupExactCollisionGame_le let w := F.encode d (γ • F.generator d) let pk := F.encodeCramerShoupPublicKey d u sk (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ())).bind fun choiceOut => let choice := choiceOut.1 @@ -677,7 +677,7 @@ private theorem succProbability_cramerShoupExactCollisionGame_le let ad := encodeAD (d, choice.1.2) let ct := F.encodeCramerShoupChallenge H d sk v w m ad ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupCollisionPhase2Oracle hasAD H isElem d sk ct ad)) (adversary.guess n choice.2 ct)).run none) >>= fun out => let target := extractCramerShoupTuple ct ad @@ -1336,10 +1336,10 @@ private theorem eval_run_interpret_map_bind (f : α → β) (oa : WordOracleComp Unit α) (s : State) (k : β × State → PMF γ) : (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) oracle) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) oracle) (f <$> oa)).run s)).bind k = (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) oracle) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) oracle) oa).run s)).bind (fun p => k (f p.1, p.2)) := by rw [OracleComp.interpret_map, StateT.run_map] simp only [← bind_pure_comp, ProbComp.eval_bind, ProbComp.eval_pure, @@ -1361,7 +1361,7 @@ private noncomputable def cramerShoupCCA2InnerB (F.encode d pkVal.1, F.encode d pkVal.2.1, F.encode d pkVal.2.2.1, F.encode d pkVal.2.2.2) m adBits β.val (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase2Oracle hasAD H isElem d sk ct adBits)) (adversary.guess n choiceOut.1.2 ct)).run ())).bind (fun guessOut => PMF.pure guessOut.1) @@ -1374,7 +1374,7 @@ private noncomputable def cramerShoupCCA2InnerSK let sk := F.skNatOfZMod d σ τ σ₁ τ₁ σ₂ τ₂ let pk := F.encodeCramerShoupPublicKey d (F.encode d (α • F.generator d)) sk (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ())).bind fun choiceOut => if isElem (d, choiceOut.1.1.1.1) && isElem (d, choiceOut.1.1.1.2) then diff --git a/Complexity/Crypto/Computational/CramerShoup/Reductions.lean b/Complexity/Crypto/Computational/CramerShoup/Reductions.lean index 142048abf1..44b66beb3e 100644 --- a/Complexity/Crypto/Computational/CramerShoup/Reductions.lean +++ b/Complexity/Crypto/Computational/CramerShoup/Reductions.lean @@ -532,7 +532,7 @@ private theorem isPPTOn_run_cramerShoupPhase1Oracle IsPPTOn encIn (encPair (encPair (encPair (encPair encMsg encMsg) encAD) encBits) (encFinEnum Unit)) (fun a => (OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem (d a) (sk a))) (adversary.choose (n a) (pk a))).run ()) := by have hp1 := ComputableTidilyInPolyTime.fst encIn encBits @@ -576,7 +576,7 @@ private theorem isPPTOn_run_cramerShoupPhase2Oracle (had : ComputableTidilyInPolyTime ad encIn encBits) : IsPPTOn encIn (encPair encBool (encFinEnum Unit)) (fun a => (OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase2Oracle hasAD H isElem (d a) (sk a) (ct a) (ad a))) (adversary.guess (n a) (state a) (ct a))).run ()) := by have hp1 := ComputableTidilyInPolyTime.fst encIn encBits @@ -623,7 +623,7 @@ private theorem isPPTOn_run_cramerShoupCollisionPhase2Oracle (had : ComputableTidilyInPolyTime ad encIn encBits) : IsPPTOn encIn (encPair encBool (encOption encBits)) (fun a => (OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupCollisionPhase2Oracle hasAD H isElem (d a) (sk a) (ct a) (ad a))) (adversary.guess (n a) (state a) (ct a))).run none) := by have hp1 := ComputableTidilyInPolyTime.fst encIn encBits @@ -695,7 +695,7 @@ noncomputable def cramerShoupMsgToDDHDistinguisher F.sampleCramerShoupSK n input.1 >>= fun sk => let pk := F.encodeCramerShoupPublicKey input.1 (csDdhU input) sk ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem input.1 sk)) (adversary.choose n pk)).run ()) >>= fun choiceOut => let choice := choiceOut.1 @@ -706,7 +706,7 @@ noncomputable def cramerShoupMsgToDDHDistinguisher let m := if bit then m₁ else m₀ let ct := F.encodeCramerShoupChallenge H input.1 sk (csDdhV input) (csDdhW input) m ad ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase2Oracle hasAD H isElem input.1 sk ct ad)) (adversary.guess n choice.2 ct)).run ()) >>= fun guessOut => pure guessOut.1 @@ -837,7 +837,7 @@ noncomputable def cramerShoupMsgToCollisionFinder let w := F.smul (d, csExpC abc, gen) let pk := F.encodeCramerShoupPublicKey d u sk ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupPhase1Oracle hasAD H isElem d sk)) (adversary.choose n pk)).run ()) >>= fun choiceOut => let choice := choiceOut.1 @@ -848,7 +848,7 @@ noncomputable def cramerShoupMsgToCollisionFinder let m := if bit then m₁ else m₀ let ct := F.encodeCramerShoupChallenge H d sk v w m ad ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (F.cramerShoupCollisionPhase2Oracle hasAD H isElem d sk ct ad)) (adversary.guess n choice.2 ct)).run none) >>= fun out => let target := extractCramerShoupTuple ct ad diff --git a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean index 2948ed2627..497248e311 100644 --- a/Complexity/Crypto/Computational/CramerShoup/Scheme.lean +++ b/Complexity/Crypto/Computational/CramerShoup/Scheme.lean @@ -364,7 +364,7 @@ theorem ADCCA2AdversaryOf.IsPPT.query_bounds {Msg AD : Type} {encMsg : Msg ↪ L (∀ n pk (State : Type) (oracle : Unit × List Bool → StateT State PMF (List Bool)) s s' choice, (choice, s') ∈ ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) oracle) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) oracle) (adversary.choose n pk)).run s).support → choice.2.length ≤ cs * (n + pk.length + 2) ^ ds) := by obtain ⟨c₁, d₁, hchoose⟩ := hA.choose.query_bounds @@ -473,7 +473,7 @@ noncomputable def cca2ADGameOn {Msg AD Out : Type} (adversary : ADCCA2AdversaryOf Msg AD) (bit : Bool) (n : ℕ) : ProbComp Bool := do let keys ← keyGen n let choiceOut ← (OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (cca2ADPhase1Oracle encOut decrypt n keys.2)) (adversary.choose n keys.1)).run () let choice := choiceOut.1 @@ -481,7 +481,7 @@ noncomputable def cca2ADGameOn {Msg AD Out : Type} let ct ← encrypt n keys.1 (if bit then csChoiceMsg₁ choice else csChoiceMsg₀ choice) (csChoiceAD choice) let guessOut ← (OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (cca2ADPhase2Oracle encOut decrypt n keys.2 ct (encAD (csChoiceAD choice)))) (adversary.guess n (csChoiceState choice) ct)).run () return guessOut.1 @@ -1608,7 +1608,7 @@ def HonestPhase2QueryBound (hasAD : Bool) {Msg AD : Type} (adversary : ADCCA2AdversaryOf Msg AD) (n Q₂ : ℕ) : Prop := ∀ d ∈ (setup n).support, ∀ α β γ δ τ δ₁ δ₂ ξ : ZMod (F.order d), ∀ choiceOut ∈ (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (fun req (s : Unit) => pure (F.cramerShoupDHPhase1Reply hasAD H isElem d α δ δ₁ δ₂ req.2, s))) (adversary.choose n diff --git a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean index dc0b185de0..acc36c2f30 100644 --- a/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean +++ b/Complexity/Crypto/Computational/Encryption/EncryptThenMAC.lean @@ -322,7 +322,7 @@ noncomputable def etmToMACForger (E : SymmetricCipher) (M : MACScheme) (tagBound else (if M.msgLen n == 0 then [false] else [], [])) <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToMACHandler E n (tagBound n) ke)) (adversary n [])).run () @@ -427,7 +427,7 @@ theorem isOraclePPT_etmToMACForger (E : SymmetricCipher) (M : MACScheme) {tagBou have hrun : IsOraclePPTOn (Operation := Unit) ECaller (encPair encBits (encFinEnum Unit)) (fun caller : (ℕ × List Bool) × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToMACHandler E caller.1.1 (tagBound caller.1.1) caller.2)) (adversary caller.1.1 [])).run ()) := by @@ -454,14 +454,14 @@ theorem isOraclePPT_etmToMACForger (E : SymmetricCipher) (M : MACScheme) {tagBou have hcBound : c.length ≤ ce * (2 * caller.1.1 + 2 * caller.2.length + request.2.length + 3) ^ de := hcLen.trans (Nat.mul_le_mul_left ce (Nat.pow_le_pow_left (by lia) de)) - obtain ⟨tag, htag, rfl⟩ := ProbOracleComp.mem_support_map hresult - obtain ⟨rawTag, _, rfl⟩ := ProbOracleComp.mem_support_map htag + obtain ⟨tag, htag, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + obtain ⟨rawTag, _, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp htag have htagTake : (List.take (tagBound caller.1.1) rawTag).length ≤ tagBound caller.1.1 := List.length_take_le _ _ refine ⟨trivial, ?_, by lia⟩ simp only [length_encPair, encBits_apply] lia - · have hresEq := ProbOracleComp.eq_of_mem_support_pure hresult + · have hresEq := OracleComp.eq_of_mem_supportWith_pure hresult subst hresEq exact ⟨trivial, by simp, by lia⟩ have hdecArg : ComputableTidilyInPolyTime @@ -537,7 +537,7 @@ theorem isOraclePPT_etmToMACForger (E : SymmetricCipher) (M : MACScheme) {tagBou else (if M.msgLen caller.1.1 == 0 then [false] else [], [])) <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToMACHandler E caller.1.1 (tagBound caller.1.1) caller.2)) (adversary caller.1.1 [])).run ()) := @@ -614,7 +614,7 @@ theorem eval_sufCmaGame_etmToMACForger (E : SymmetricCipher) (M : MACScheme) ProbComp.eval_bind, ProbComp.eval_pure, ProbOracleComp.eval_run_interpret] have hinner (km : List Bool) : ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (M.signingPairOracle km q s))) (do let ke ← ProbOracleComp.sample (E.keyGen n) @@ -625,7 +625,7 @@ theorem eval_sufCmaGame_etmToMACForger (E : SymmetricCipher) (M : MACScheme) else (if M.msgLen n == 0 then [false] else [], [])) <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToMACHandler E n (tagBound n) ke)) (adversary n [])).run ())).run []).bind @@ -634,10 +634,10 @@ theorem eval_sufCmaGame_etmToMACForger (E : SymmetricCipher) (M : MACScheme) M.verify km out.1.1 out.1.2)) = (ProbComp.eval (E.keyGen n)).bind (fun ke => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (M.signingPairOracle km q s))) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToMACHandler E n (tagBound n) ke)) (adversary n [])).run ())).run []).bind @@ -674,7 +674,7 @@ theorem eval_sufCmaGame_etmToMACForger (E : SymmetricCipher) (M : MACScheme) have hsim := ProbOracleComp.run_interpret_map_state (oracle := fun q (state : Unit × List (List Bool × List Bool)) => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (M.signingPairOracle km q s))) (etmToMACHandler E n (tagBound n) ke q state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -760,12 +760,12 @@ theorem isQueryBounded_etmToMACForger (E : SymmetricCipher) (M : MACScheme) refine OracleComp.IsCostBounded.run_interpret (fun q s => ?_) hq () cases q with | inl m => - simp only [ProbOracleComp.handler, Sum.elim_inl] + simp only [OracleComp.sumHandler, Sum.elim_inl] change ((·, s) <$> ProbOracleComp.sample (ProbComp.unifFin m)).IsQueryBounded 0 simp only [OracleComp.isCostBounded_map_iff] exact ProbOracleComp.IsQueryBounded.sample (ProbComp.unifFin m) | inr request => - simp only [ProbOracleComp.handler, Sum.elim_inr] + simp only [OracleComp.sumHandler, Sum.elim_inr] exact isQueryBounded_etmToMACHandler E n (tagBound n) ke request s /-- Open stateful handler that simulates the `oneTimeCIEncryptionOracle` of `encryptThenMAC E M` @@ -802,7 +802,7 @@ noncomputable def etmToOneTimeMACForger (E : SymmetricCipher) (M : MACScheme) (t else (if M.msgLen n == 0 then [false] else [], [])) <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeMACHandler E n (tagBound n) ke)) (adversary n [])).run false @@ -908,7 +908,7 @@ theorem isOraclePPT_etmToOneTimeMACForger (E : SymmetricCipher) (M : MACScheme) have hrun : IsOraclePPTOn (Operation := Unit) ECaller (encPair encBits encBool) (fun caller : (ℕ × List Bool) × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeMACHandler E caller.1.1 (tagBound caller.1.1) caller.2)) (adversary caller.1.1 [])).run false) := by @@ -935,14 +935,14 @@ theorem isOraclePPT_etmToOneTimeMACForger (E : SymmetricCipher) (M : MACScheme) have hcBound : c.length ≤ ce * (2 * caller.1.1 + 2 * caller.2.length + request.2.length + 3) ^ de := hcLen.trans (Nat.mul_le_mul_left ce (Nat.pow_le_pow_left (by lia) de)) - obtain ⟨tag, htag, rfl⟩ := ProbOracleComp.mem_support_map hresult - obtain ⟨rawTag, _, rfl⟩ := ProbOracleComp.mem_support_map htag + obtain ⟨tag, htag, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + obtain ⟨rawTag, _, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp htag have htagTake : (List.take (tagBound caller.1.1) rawTag).length ≤ tagBound caller.1.1 := List.length_take_le _ _ refine ⟨trivial, ?_, by simp [encBool_apply]⟩ simp only [length_encPair, encBits_apply] lia - · have hresEq := ProbOracleComp.eq_of_mem_support_pure hresult + · have hresEq := OracleComp.eq_of_mem_supportWith_pure hresult subst hresEq exact ⟨trivial, by simp, by simp [encBool_apply]⟩ have hdecArg : ComputableTidilyInPolyTime @@ -1018,7 +1018,7 @@ theorem isOraclePPT_etmToOneTimeMACForger (E : SymmetricCipher) (M : MACScheme) else (if M.msgLen caller.1.1 == 0 then [false] else [], [])) <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeMACHandler E caller.1.1 (tagBound caller.1.1) caller.2)) (adversary caller.1.1 [])).run false) := @@ -1051,12 +1051,12 @@ theorem isQueryBounded_etmToOneTimeMACForger (E : SymmetricCipher) (M : MACSchem refine OracleComp.IsCostBounded.run_interpret (fun q s => ?_) hq false cases q with | inl m => - simp only [ProbOracleComp.handler, Sum.elim_inl] + simp only [OracleComp.sumHandler, Sum.elim_inl] change ((·, s) <$> ProbOracleComp.sample (ProbComp.unifFin m)).IsQueryBounded 0 simp only [OracleComp.isCostBounded_map_iff] exact ProbOracleComp.IsQueryBounded.sample (ProbComp.unifFin m) | inr request => - simp only [ProbOracleComp.handler, Sum.elim_inr] + simp only [OracleComp.sumHandler, Sum.elim_inr] exact isQueryBounded_etmToOneTimeMACHandler E n (tagBound n) ke request s private noncomputable def etmOneTimeMACIntermediateOracle (E : SymmetricCipher) (M : MACScheme) @@ -1088,7 +1088,7 @@ theorem eval_sufOneTimeGame_etmToOneTimeMACForger (E : SymmetricCipher) (M : MAC ProbComp.eval_bind, ProbComp.eval_pure, ProbOracleComp.eval_run_interpret] have hinner (km : List Bool) : ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (M.oneTimeSigningPairOracle km q s))) (do let ke ← ProbOracleComp.sample (E.keyGen n) @@ -1099,7 +1099,7 @@ theorem eval_sufOneTimeGame_etmToOneTimeMACForger (E : SymmetricCipher) (M : MAC else (if M.msgLen n == 0 then [false] else [], [])) <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeMACHandler E n (tagBound n) ke)) (adversary n [])).run false)).run []).bind @@ -1108,10 +1108,10 @@ theorem eval_sufOneTimeGame_etmToOneTimeMACForger (E : SymmetricCipher) (M : MAC M.verify km out.1.1 out.1.2)) = (ProbComp.eval (E.keyGen n)).bind (fun ke => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (M.oneTimeSigningPairOracle km q s))) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeMACHandler E n (tagBound n) ke)) (adversary n [])).run false)).run []).bind @@ -1149,7 +1149,7 @@ theorem eval_sufOneTimeGame_etmToOneTimeMACForger (E : SymmetricCipher) (M : MAC (oracle := etmOneTimeMACIntermediateOracle E M n ke km) (oracle' := fun q (state : Bool × List (List Bool × List Bool)) => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (M.oneTimeSigningPairOracle km q s))) ((etmToOneTimeMACHandler E n (tagBound n) ke q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -1160,7 +1160,7 @@ theorem eval_sufOneTimeGame_etmToOneTimeMACForger (E : SymmetricCipher) (M : MAC change (etmOneTimeMACIntermediateOracle E M n ke km ((), msg) queriedPairs).map (fun x => (x.1, !x.2.isEmpty, x.2)) = ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (M.oneTimeSigningPairOracle km q s))) (etmToOneTimeMACHandler E n (tagBound n) ke ((), msg) (!queriedPairs.isEmpty))).run queriedPairs).map @@ -1259,7 +1259,7 @@ noncomputable def etmToCPAAdversary (M : MACScheme) (adversary : OracleDistingui fun n _ => do let km ← ProbOracleComp.sample (M.keyGen n) Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToCPAHandler M n km)) (adversary n [])).run () @@ -1361,7 +1361,7 @@ theorem isOraclePPT_etmToCPAAdversary (M : MACScheme) {adversary : OracleDisting have hrun : IsOraclePPTOn (Operation := Unit) ECaller (encPair encBool (encFinEnum Unit)) (fun caller : (ℕ × List Bool) × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToCPAHandler M caller.1.1 caller.2)) (adversary caller.1.1 [])).run ()) := by @@ -1381,11 +1381,11 @@ theorem isOraclePPT_etmToCPAAdversary (M : MACScheme) {adversary : OracleDisting dsimp only at hresult split_ifs at hresult with hlenEq · obtain ⟨c, hc, hresult⟩ := OracleComp.mem_supportWith_bind_iff.mp hresult - obtain ⟨rawCt, _, rfl⟩ := ProbOracleComp.mem_support_map hc + obtain ⟨rawCt, _, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hc have hcTake : (List.take (M.msgLen caller.1.1) rawCt).length ≤ M.msgLen caller.1.1 := List.length_take_le _ _ - obtain ⟨tag, htag, rfl⟩ := ProbOracleComp.mem_support_map hresult - rw [ProbOracleComp.support_sample] at htag + obtain ⟨tag, htag, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + simp only [ProbOracleComp.support_sample] at htag have htagLen := hlenSign (caller.2, List.take (M.msgLen caller.1.1) rawCt) tag htag simp only [length_encPair, encBits_apply] at htagLen have htagBound : tag.length ≤ cs * (2 * caller.2.length + M.msgLen caller.1.1 + 2) ^ ds := @@ -1393,13 +1393,13 @@ theorem isOraclePPT_etmToCPAAdversary (M : MACScheme) {adversary : OracleDisting refine ⟨trivial, ?_, by lia⟩ simp only [length_encPair, encBits_apply] lia - · have hresEq := ProbOracleComp.eq_of_mem_support_pure hresult + · have hresEq := OracleComp.eq_of_mem_supportWith_pure hresult subst hresEq exact ⟨trivial, by simp, by lia⟩ have hrunMap : IsOraclePPTOn (Operation := Unit) ECaller encBool (fun caller : (ℕ × List Bool) × List Bool => Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToCPAHandler M caller.1.1 caller.2)) (adversary caller.1.1 [])).run ()) := @@ -1437,7 +1437,7 @@ theorem eval_cpaGame_etmToCPAAdversary (E : SymmetricCipher) (M : MACScheme) have hsim := ProbOracleComp.run_interpret_map_state (oracle := fun q (state : Unit × Unit) => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (E.cpaEncryptionOracle n ke bit q s))) (etmToCPAHandler M n km q state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -1531,12 +1531,12 @@ theorem isQueryBounded_etmToCPAAdversary (M : MACScheme) (adversary : OracleDist refine OracleComp.IsCostBounded.run_interpret (fun q s => ?_) hq () cases q with | inl m => - simp only [ProbOracleComp.handler, Sum.elim_inl] + simp only [OracleComp.sumHandler, Sum.elim_inl] change ((·, s) <$> ProbOracleComp.sample (ProbComp.unifFin m)).IsQueryBounded 0 simp only [OracleComp.isCostBounded_map_iff] exact ProbOracleComp.IsQueryBounded.sample (ProbComp.unifFin m) | inr request => - simp only [ProbOracleComp.handler, Sum.elim_inr] + simp only [OracleComp.sumHandler, Sum.elim_inr] exact isQueryBounded_etmToCPAHandler M n km request s /-- Open stateful handler that simulates the `oneTimeCPAEncryptionOracle` of `encryptThenMAC E M` @@ -1568,7 +1568,7 @@ noncomputable def etmToOneTimeCPAAdversary (M : MACScheme) (adversary : OracleDi fun n _ => do let km ← ProbOracleComp.sample (M.keyGen n) Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeCPAHandler M n km)) (adversary n [])).run false @@ -1671,7 +1671,7 @@ theorem isOraclePPT_etmToOneTimeCPAAdversary (M : MACScheme) {adversary : Oracle have hrun : IsOraclePPTOn (Operation := Unit) ECaller (encPair encBool encBool) (fun caller : (ℕ × List Bool) × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeCPAHandler M caller.1.1 caller.2)) (adversary caller.1.1 [])).run false) := by @@ -1691,11 +1691,11 @@ theorem isOraclePPT_etmToOneTimeCPAAdversary (M : MACScheme) {adversary : Oracle dsimp only at hresult split_ifs at hresult with hlenEq · obtain ⟨c, hc, hresult⟩ := OracleComp.mem_supportWith_bind_iff.mp hresult - obtain ⟨rawCt, _, rfl⟩ := ProbOracleComp.mem_support_map hc + obtain ⟨rawCt, _, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hc have hcTake : (List.take (M.msgLen caller.1.1) rawCt).length ≤ M.msgLen caller.1.1 := List.length_take_le _ _ - obtain ⟨tag, htag, rfl⟩ := ProbOracleComp.mem_support_map hresult - rw [ProbOracleComp.support_sample] at htag + obtain ⟨tag, htag, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + simp only [ProbOracleComp.support_sample] at htag have htagLen := hlenSign (caller.2, List.take (M.msgLen caller.1.1) rawCt) tag htag simp only [length_encPair, encBits_apply] at htagLen have htagBound : tag.length ≤ cs * (2 * caller.2.length + M.msgLen caller.1.1 + 2) ^ ds := @@ -1703,13 +1703,13 @@ theorem isOraclePPT_etmToOneTimeCPAAdversary (M : MACScheme) {adversary : Oracle refine ⟨trivial, ?_, by simp [encBool_apply]⟩ simp only [length_encPair, encBits_apply] lia - · have hresEq := ProbOracleComp.eq_of_mem_support_pure hresult + · have hresEq := OracleComp.eq_of_mem_supportWith_pure hresult subst hresEq exact ⟨trivial, by simp, by simp [encBool_apply]⟩ have hrunMap : IsOraclePPTOn (Operation := Unit) ECaller encBool (fun caller : (ℕ × List Bool) × List Bool => Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (etmToOneTimeCPAHandler M caller.1.1 caller.2)) (adversary caller.1.1 [])).run false) := @@ -1754,12 +1754,12 @@ theorem isQueryBounded_etmToOneTimeCPAAdversary (M : MACScheme) (adversary : Ora refine OracleComp.IsCostBounded.run_interpret (fun q s => ?_) hq false cases q with | inl m => - simp only [ProbOracleComp.handler, Sum.elim_inl] + simp only [OracleComp.sumHandler, Sum.elim_inl] change ((·, s) <$> ProbOracleComp.sample (ProbComp.unifFin m)).IsQueryBounded 0 simp only [OracleComp.isCostBounded_map_iff] exact ProbOracleComp.IsQueryBounded.sample (ProbComp.unifFin m) | inr request => - simp only [ProbOracleComp.handler, Sum.elim_inr] + simp only [OracleComp.sumHandler, Sum.elim_inr] exact isQueryBounded_etmToOneTimeCPAHandler M n km request s /-- Running `etmToOneTimeCPAAdversary M adversary` in `E.cpaOneTimeGame` at challenge bit `bit` @@ -1795,7 +1795,7 @@ theorem eval_cpaOneTimeGame_etmToOneTimeCPAAdversary (E : SymmetricCipher) (M : (encPair encBits encBits (ke, km)) bit q alreadyQueried)) (oracle' := fun q (state : Bool × Bool) => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (E.oneTimeCPAEncryptionOracle n ke bit q s))) ((etmToOneTimeCPAHandler M n km q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -1806,7 +1806,7 @@ theorem eval_cpaOneTimeGame_etmToOneTimeCPAAdversary (E : SymmetricCipher) (M : (encPair encBits encBits (ke, km)) bit ((), payload) alreadyQueried)).map (fun x => (x.1, x.2, x.2)) = ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun q s => ProbComp.eval (E.oneTimeCPAEncryptionOracle n ke bit q s))) (etmToOneTimeCPAHandler M n km ((), payload) alreadyQueried)).run alreadyQueried).map (fun result => (result.1.1, result.1.2, result.2)) @@ -2202,7 +2202,7 @@ noncomputable def cpaToPrfDistinguisher (adversary : OracleDistinguisher) (bit : fun n _ => Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (cpaToPrfHandler n bit)) (adversary n [])).run () @@ -2283,7 +2283,7 @@ theorem isOraclePPT_cpaToPrfDistinguisher {adversary : OracleDistinguisher} have hrun : IsOraclePPTOn (Operation := Unit) ECaller (encPair encBool (encFinEnum Unit)) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (cpaToPrfHandler caller.1 bit)) (adversary caller.1 [])).run ()) := by @@ -2306,13 +2306,13 @@ theorem isOraclePPT_cpaToPrfDistinguisher {adversary : OracleDistinguisher} (ProbOracleComp.sample (BitString.sampleList caller.1)) at hr rw [ProbOracleComp.support_sample, BitString.eval_sampleList] at hr have hrLen : r.length = caller.1 := BitString.length_of_mem_support_uniformList hr - obtain ⟨pad, hpad, rfl⟩ := ProbOracleComp.mem_support_map hresult - obtain ⟨rawPad, _, rfl⟩ := ProbOracleComp.mem_support_map hpad + obtain ⟨pad, hpad, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + obtain ⟨rawPad, _, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hpad have hpadTake : (List.take caller.1 rawPad).length ≤ caller.1 := List.length_take_le _ _ simp only [List.length_append, List.length_zipWith, hrLen] exact ⟨trivial, by lia, Nat.le_add_right _ _⟩ · simp only [hlenEq, Bool.false_eq_true, ↓reduceIte] at hresult - have hresEq := ProbOracleComp.eq_of_mem_support_pure hresult + have hresEq := OracleComp.eq_of_mem_supportWith_pure hresult subst hresEq exact ⟨trivial, by simp, Nat.le_add_right _ _⟩ unfold cpaToPrfDistinguisher @@ -2336,7 +2336,7 @@ theorem eval_prfRealGame_cpaToPrfDistinguisher (family : List Bool → List Bool have hread := ProbOracleComp.run_interpret_readOnly (fun req (_ : Unit) => PMF.pure (prfOracle family n k req.2)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun m => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin m))) (cpaToPrfHandler n bit)) (adversary n [])).run ()) () @@ -2350,7 +2350,7 @@ theorem eval_prfRealGame_cpaToPrfDistinguisher (family : List Bool → List Bool have hsim := ProbOracleComp.run_interpret_map_state (oracle := fun q (state : Unit × Unit) => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun req (s : Unit) => (PMF.pure (prfOracle family n k req.2)).map (·, s))) (cpaToPrfHandler n bit q state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -2439,7 +2439,7 @@ private theorem eval_prfIdealGame_cpaToPrfDistinguisher (adversary : OracleDisti (bit : Bool) (n : ℕ) : ProbComp.eval (prfIdealGame (cpaToPrfDistinguisher adversary bit) n) = ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherFaithfulWithBadOracle n bit)) (adversary n [])).run ([], false)).map Prod.fst := by rw [prfIdealGame_eq_cached, ProbComp.eval_map, ProbOracleComp.eval_run_interpret] @@ -2449,7 +2449,7 @@ private theorem eval_prfIdealGame_cpaToPrfDistinguisher (adversary : OracleDisti have hsim := ProbOracleComp.run_interpret_map_state (oracle := fun q (state : Unit × List (List Bool × List Bool)) => ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (fun req s => ProbComp.eval (cachedRandomFunctionOracle n req.2 s))) (cpaToPrfHandler n bit q state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -2496,11 +2496,11 @@ private theorem eval_prfIdealGame_cpaToPrfDistinguisher (adversary : OracleDisti private theorem run_prfCipherForgetfulWithBadOracle_map_fst (adversary : OracleDistinguisher) (bit : Bool) (n : ℕ) (cache : List (List Bool × List Bool)) (bad : Bool) : ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit)) (adversary n [])).run (cache, bad)).map Prod.fst = ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherOTPOracle n)) (adversary n [])).run ()).map Prod.fst := by have hsim := ProbOracleComp.run_interpret_map_state @@ -2534,9 +2534,9 @@ private theorem run_prfCipherForgetfulWithBadOracle_map_fst (adversary : OracleD private theorem identicalUntilBad_prfCipherFaithful_forgetful (n : ℕ) (bit : Bool) : OracleComp.IdenticalUntilBad - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherFaithfulWithBadOracle n bit)) - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit)) (fun s => s.2 = true) where agree q s hs a s' hs' := by @@ -2548,7 +2548,7 @@ private theorem identicalUntilBad_prfCipherFaithful_forgetful (n : ℕ) (bit : B have hbad : bad = false := Bool.eq_false_iff.mpr hs have hbad' : bad' = false := Bool.eq_false_iff.mpr hs' subst hbad hbad' - simp only [ProbOracleComp.handler, prfCipherFaithfulWithBadOracle, + simp only [OracleComp.sumHandler, prfCipherFaithfulWithBadOracle, prfCipherForgetfulWithBadOracle, Bool.false_or] by_cases hlenEq : ((unframe request.2).length == n && (dropFrame request.2).length == n) = true @@ -2579,7 +2579,7 @@ private theorem identicalUntilBad_prfCipherFaithful_forgetful (n : ℕ) (bit : B rcases s with ⟨cache, bad⟩ simp only at hs subst hs - simp only [ProbOracleComp.handler, prfCipherFaithfulWithBadOracle, Bool.true_or] at hx + simp only [OracleComp.sumHandler, prfCipherFaithfulWithBadOracle, Bool.true_or] at hx by_cases hlenEq : ((unframe request.2).length == n && (dropFrame request.2).length == n) = true · simp only [hlenEq, ↓reduceIte] at hx @@ -2599,7 +2599,7 @@ private theorem identicalUntilBad_prfCipherFaithful_forgetful (n : ℕ) (bit : B rcases s with ⟨cache, bad⟩ simp only at hs subst hs - simp only [ProbOracleComp.handler, prfCipherForgetfulWithBadOracle, Bool.true_or] at hx + simp only [OracleComp.sumHandler, prfCipherForgetfulWithBadOracle, Bool.true_or] at hx by_cases hlenEq : ((unframe request.2).length == n && (dropFrame request.2).length == n) = true · simp only [hlenEq, ↓reduceIte] at hx @@ -2673,7 +2673,7 @@ private theorem bad_prfCipherForgetfulWithBadOracle_le {α : Type} (n : ℕ) (bi {program : WordOracleComp Unit α} {Q : ℕ} (hq : program.IsQueryBounded Q) (cache : List (List Bool × List Bool)) : ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit)) program).run (cache, false)).toOuterMeasure {x | x.2.2 = true} ≤ (Q : ℝ≥0∞) * ((cache.length + Q : ℕ) : ℝ≥0∞) * ((1 : ℝ≥0∞) / 2 ^ n) := by @@ -2688,16 +2688,16 @@ private theorem bad_prfCipherForgetfulWithBadOracle_le {α : Type} (n : ℕ) (bi | inl m => simp only [Sum.elim_inl, Nat.add_zero] set B : ℝ≥0∞ := (Q : ℝ≥0∞) * ((cache.length + Q : ℕ) : ℝ≥0∞) * ((1 : ℝ≥0∞) / 2 ^ n) - calc ∑' y, ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + calc ∑' y, OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit) (Sum.inl m) (cache, false) y * ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit)) (cont y.1)).run y.2).toOuterMeasure {x | x.2.2 = true} - ≤ ∑' y, ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + ≤ ∑' y, OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit) (Sum.inl m) (cache, false) y * B := by refine tsum_le_tsum fun y => ?_ - by_cases hy : y ∈ (ProbOracleComp.handler + by_cases hy : y ∈ (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit) (Sum.inl m) (cache, false)).support · change y ∈ ((ProbComp.unifOracle m).map (·, (cache, false))).support at hy @@ -2714,7 +2714,7 @@ private theorem bad_prfCipherForgetfulWithBadOracle_le {α : Type} (n : ℕ) (bi have hterm (y : List Bool × (List (List Bool × List Bool) × Bool)) : prfCipherForgetfulWithBadOracle n bit request (cache, false) y * ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit)) (cont y.1)).run y.2).toOuterMeasure {x | x.2.2 = true} ≤ prfCipherForgetfulWithBadOracle n bit request (cache, false) y * @@ -2742,7 +2742,7 @@ private theorem bad_prfCipherForgetfulWithBadOracle_le {α : Type} (n : ℕ) (bi · rw [(PMF.apply_eq_zero_iff _ _).mpr hmem, zero_mul, zero_mul] calc ∑' y, prfCipherForgetfulWithBadOracle n bit request (cache, false) y * ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit)) (cont y.1)).run y.2).toOuterMeasure {x | x.2.2 = true} ≤ ∑' y, prfCipherForgetfulWithBadOracle n bit request (cache, false) y * @@ -2784,7 +2784,7 @@ private theorem advantage_prfIdealGame_prfCipherOTPOracle_le (adversary : Oracle (Game.advantage (ProbComp.eval (prfIdealGame (cpaToPrfDistinguisher adversary bit) n)) (((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherOTPOracle n)) (adversary n [])).run ()).map Prod.fst) : ℝ) ≤ (Q : ℝ) ^ 2 / (2 : ℝ) ^ n := by @@ -2794,11 +2794,11 @@ private theorem advantage_prfIdealGame_prfCipherOTPOracle_le (adversary : Oracle have hadv := hiub.advantage_le (adversary n []) ([], false) (fun out => PMF.pure out.1) change (Game.advantage (((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherFaithfulWithBadOracle n bit)) (adversary n [])).run ([], false)).map Prod.fst) (((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherForgetfulWithBadOracle n bit)) (adversary n [])).run ([], false)).map Prod.fst) : ℝ) ≤ _ at hadv rw [hiub.bad_eq] at hadv @@ -2844,7 +2844,7 @@ theorem advantage_cpaGame_prfCipher_le (family : List Bool → List Bool → Lis let pReal1 := ProbComp.eval (prfRealGame family (cpaToPrfDistinguisher adversary true) n) let pIdeal1 := ProbComp.eval (prfIdealGame (cpaToPrfDistinguisher adversary true) n) let pOTP := ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifOracle m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifOracle m)) (prfCipherOTPOracle n)) (adversary n [])).run ()).map Prod.fst change (Game.advantage pReal0 pReal1 : ℝ) ≤ diff --git a/Complexity/Crypto/Computational/GGM/Expansion.lean b/Complexity/Crypto/Computational/GGM/Expansion.lean index b0bc21494d..babcb91a8c 100644 --- a/Complexity/Crypto/Computational/GGM/Expansion.lean +++ b/Complexity/Crypto/Computational/GGM/Expansion.lean @@ -67,7 +67,7 @@ def expansionGame (generator : List Bool → List Bool) (sample : ProbComp (List Bool)) (adversary : OracleDistinguisher) (n depth : ℕ) : ProbComp Bool := Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (fun request => expansionOracle generator sample n depth request.2)) (adversary n [])).run [] @@ -151,7 +151,7 @@ theorem isPPTOn_expansionGame {Caller : Type} {input : Caller ↪ List Bool} have hdepth := hdepth.tidy have hrun : IsPPTOn input (encPair encBool cacheEncoding) (fun a => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (fun request => expansionOracle generator (sample a) (width a) (depth a) request.2)) (adversary (width a) [])).run []) := by apply hadversary.run_interpret_preprocess (operationEncoding := encFinEnum Unit) @@ -242,10 +242,10 @@ theorem expansionGame_generated (generator : List Bool → List Bool) private theorem prefix_eager (n depth width : ℕ) (hdepth : depth ≤ n) (respond : List Bool → List Bool → List Bool) (program : WordOracleComp Unit Bool) : (PMF.uniformOfFintype (BitString depth → BitString width)).bind (fun table => - OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle (fun request => + OracleComp.interpret (OracleComp.sumHandler ProbComp.unifOracle (fun request => PMF.pure (if request.2.length = n then respond request.2 (List.ofFn (table (BitString.ofList depth (request.2.take depth)))) else []))) program) = - ((OracleComp.interpret (ProbOracleComp.handler + ((OracleComp.interpret (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun request cache => if request.2.length = n then (memoize (fun _ : List Bool => BitString.uniformList width) @@ -260,10 +260,10 @@ private theorem prefix_eager (n depth width : ℕ) (hdepth : depth ≤ n) (⟨List.ofFn, List.ofFn_injective⟩ : BitString depth ↪ List Bool) List.ofFn (fun _ => PMF.uniformOfFintype (BitString width)) (fun _ => BitString.uniformList width) (fun _ => rfl) (OracleComp.interpret - (ProbOracleComp.handler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) (fun request : Unit × List Bool => adapter request.2)) program) have hstep (query : List Bool) : OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun key => memoize (fun _ : List Bool => BitString.uniformList width) (List.ofFn key))) (adapter query) = fun cache => if query.length = n then (memoize (fun _ : List Bool => BitString.uniformList width) (query.take depth) cache).map @@ -279,7 +279,7 @@ private theorem prefix_eager (n depth width : ℕ) (hdepth : depth ≤ n) rfl have heval (table : BitString depth → BitString width) (query : List Bool) : OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifOracle (fun key => PMF.pure (List.ofFn (table key)))) + (OracleComp.sumHandler ProbComp.unifOracle (fun key => PMF.pure (List.ofFn (table key)))) (adapter query) = PMF.pure (if query.length = n then respond query (List.ofFn (table (BitString.ofList depth (query.take depth)))) else []) := by by_cases hquery : query.length = n <;> simp [adapter, hquery, PMF.pure_map] @@ -338,12 +338,12 @@ theorem expansionGame_uniform (generator : List Bool → List Bool) (adversary : ProbComp.eval (expansionGame generator (BitString.sampleList (2 * n)) adversary n depth) = ProbComp.eval (hybridGame generator adversary n (depth + 1)) := by let earlier := fun table : BitString depth → BitString (2 * n) => - OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle (fun request => + OracleComp.interpret (OracleComp.sumHandler ProbComp.unifOracle (fun request => PMF.pure (if request.2.length = n then eval generator (selectChild n (List.ofFn (table (BitString.ofList depth (request.2.take depth)))) (request.2[depth]?.getD false)) (request.2.drop (depth + 1)) else []))) (adversary n []) let later := fun table : BitString (depth + 1) → BitString n => - OracleComp.interpret (ProbOracleComp.handler ProbComp.unifOracle (fun request => + OracleComp.interpret (OracleComp.sumHandler ProbComp.unifOracle (fun request => PMF.pure (if request.2.length = n then eval generator (List.ofFn (table (BitString.ofList (depth + 1) (request.2.take (depth + 1))))) (request.2.drop (depth + 1)) else []))) (adversary n []) diff --git a/Complexity/Crypto/Computational/GGM/Hybrid.lean b/Complexity/Crypto/Computational/GGM/Hybrid.lean index 73dcbf8854..c9d04dcfcc 100644 --- a/Complexity/Crypto/Computational/GGM/Hybrid.lean +++ b/Complexity/Crypto/Computational/GGM/Hybrid.lean @@ -73,7 +73,7 @@ noncomputable def frontierOracle (generator : List Bool → List Bool) (n depth noncomputable def hybridGame (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n depth : ℕ) : ProbComp Bool := Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (fun request => frontierOracle generator n depth request.2)) (adversary n [])).run [] /-- At level zero, all valid queries share one root label. Sampling that label on demand agrees @@ -182,7 +182,7 @@ theorem isPPTOn_hybridGame {generator : List Bool → List Bool} have hgenerator := hgenerator.tidy have hrun : IsPPTOn (encPair encUnary encUnary) (encPair encBool cacheEncoding) (fun pair : ℕ × ℕ => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (fun request => frontierOracle generator pair.1 pair.2 request.2)) (adversary pair.1 [])).run []) := by apply hadversary.run_interpret_preprocess (operationEncoding := encFinEnum Unit) diff --git a/Complexity/Crypto/Computational/GGM/Reduction.lean b/Complexity/Crypto/Computational/GGM/Reduction.lean index 134b72c398..9aba902342 100644 --- a/Complexity/Crypto/Computational/GGM/Reduction.lean +++ b/Complexity/Crypto/Computational/GGM/Reduction.lean @@ -53,7 +53,7 @@ Truncation and the empty fallback make the test total on every challenge list. - def sampleGame (generator : List Bool → List Bool) (adversary : OracleDistinguisher) (n depth : ℕ) (values : List (List Bool)) : ProbComp Bool := Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (OracleComp.withSampleList [] (fun expansion request => expansionOracle generator (pure expansion) n depth request.2))) (adversary n [])).run ([], values) @@ -102,7 +102,7 @@ theorem isPPTOn_sampleGame {Caller : Type} {input : Caller ↪ List Bool} have hrun : IsPPTOn input (encPair encBool (encPair cacheEncoding (encList encBits))) (fun a => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (OracleComp.withSampleList [] (fun expansion request => expansionOracle generator (pure expansion) (width a) (depth a) request.2))) (adversary (width a) [])).run ([], values a)) := by diff --git a/Complexity/Crypto/Computational/GMW/Protocol.lean b/Complexity/Crypto/Computational/GMW/Protocol.lean index 91e060f77e..8a9099724c 100644 --- a/Complexity/Crypto/Computational/GMW/Protocol.lean +++ b/Complexity/Crypto/Computational/GMW/Protocol.lean @@ -597,7 +597,7 @@ def twoRoundStep (reply1 reply2 : List Bool → List Bool) (q : List Bool) /-- Run a `WordOracleComp Unit` program against `twoRoundStep` inside `ProbComp`. -/ def runTwoRound {α : Type} (reply1 reply2 : List Bool → List Bool) (prog : WordOracleComp Unit α) (s : ℕ × List Bool) : ProbComp (α × (ℕ × List Bool)) := - (OracleComp.interpret (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifFin n)) + (OracleComp.interpret (OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifFin n)) (fun q state => pure (twoRoundStep reply1 reply2 q.2 state))) prog).run s @[simp] theorem runTwoRound_pure {α : Type} (reply1 reply2 : List Bool → List Bool) @@ -694,7 +694,7 @@ theorem run_gmwProver_fst {α : Type} (generator : List Bool → List Bool) (s m simp [P, gmwProver, relate, oracle', PMF.bind_map, Function.comp_def]) prog P.init have hmap := congrArg (PMF.map Prod.fst) hsim have hlhs : (((OracleComp.interpret - (ProbOracleComp.handler (fun n => StateT.lift (ProbComp.unifOracle n)) P.respond) + (OracleComp.sumHandler (fun n => StateT.lift (ProbComp.unifOracle n)) P.respond) prog).run P.init).bind (fun (a, s') => (relate s').map (a, ·))).map Prod.fst = (P.run prog P.init).map Prod.fst := by simp only [Prover.run, PMF.map_bind, PMF.map_comp, Function.comp_def] diff --git a/Complexity/Crypto/Computational/GMW/Simulator.lean b/Complexity/Crypto/Computational/GMW/Simulator.lean index c365b4c3d6..4b8a0221ed 100644 --- a/Complexity/Crypto/Computational/GMW/Simulator.lean +++ b/Complexity/Crypto/Computational/GMW/Simulator.lean @@ -90,7 +90,7 @@ private theorem runTwoRound_query_inl {α β : Type} (reply1 reply2 : List Bool f <$> runTwoRound reply1 reply2 (OracleComp.query (Sum.inl n) >>= k) s = (ProbComp.unifFin n >>= fun u => f <$> runTwoRound reply1 reply2 (k u) s) := by simp only [runTwoRound, OracleComp.interpret_bind, OracleComp.interpret_query, - ProbOracleComp.handler, StateT.run_bind, StateT.run_lift, bind_assoc, pure_bind, map_bind] + OracleComp.sumHandler, StateT.run_bind, StateT.run_lift, bind_assoc, pure_bind, map_bind] private theorem runTwoRound_query_inr {α β : Type} (reply1 reply2 : List Bool → List Bool) (q : Unit × List Bool) (k : List Bool → WordOracleComp Unit α) (s : ℕ × List Bool) @@ -99,7 +99,7 @@ private theorem runTwoRound_query_inr {α β : Type} (reply1 reply2 : List Bool let step := twoRoundStep reply1 reply2 q.2 s f <$> runTwoRound reply1 reply2 (k step.1) step.2 := by simp only [runTwoRound, OracleComp.interpret_bind, OracleComp.interpret_query, - ProbOracleComp.handler, StateT.run_bind] + OracleComp.sumHandler, StateT.run_bind] rfl private theorem length_snd_mem_support_runTwoRound {α : Type} (r1 r2 : List Bool → List Bool) diff --git a/Complexity/Crypto/Computational/IndexedSignature.lean b/Complexity/Crypto/Computational/IndexedSignature.lean index 6e079b1753..c53cfaf388 100644 --- a/Complexity/Crypto/Computational/IndexedSignature.lean +++ b/Complexity/Crypto/Computational/IndexedSignature.lean @@ -140,7 +140,7 @@ def indexedEufCmaGame (S : IndexedSignatureScheme) (adversary : IndexedForger) ( ProbComp Bool := do let keys ← S.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.indexedSigningOracle n keys.2)) (adversary n keys.1)).run [] return !out.2.contains (out.1.1, out.1.2.1) && S.verify keys.1 out.1.1 out.1.2.1 out.1.2.2 @@ -154,7 +154,7 @@ theorem isPPTOn_run_indexedSigningOracle (S : IndexedSignatureScheme) {adversary (encPair (encPair encUnary (encPair encBits encBits)) (encList (encPair encUnary encBits))) (fun caller : ℕ × (List Bool × List Bool) => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.indexedSigningOracle caller.1 caller.2.2)) (adversary caller.1 caller.2.1)).run []) := by obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le diff --git a/Complexity/Crypto/Computational/IndexedSignature/Counter.lean b/Complexity/Crypto/Computational/IndexedSignature/Counter.lean index 9088156c1f..0de3689f54 100644 --- a/Complexity/Crypto/Computational/IndexedSignature/Counter.lean +++ b/Complexity/Crypto/Computational/IndexedSignature/Counter.lean @@ -109,7 +109,7 @@ that was never signed, of any length. -/ def counterEufCmaGame (adversary : Forger) (n : ℕ) : ProbComp Bool := do let keys ← S.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.counterSigningOracle n keys.2)) (adversary n keys.1)).run (0, []) return !out.2.2.contains out.1.1 && S.counterVerify keys.1 out.1.1 out.1.2 @@ -149,7 +149,7 @@ theorem isPPTOn_run_counterSigningOracle {adversary : Forger} (encPair (encPair encBits encBits) (encPair encUnary (encList encBits))) (fun caller : ℕ × (List Bool × List Bool) => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.counterSigningOracle caller.1 caller.2.2)) (adversary caller.1 caller.2.1)).run (0, [])) := by obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le @@ -278,7 +278,7 @@ variable (S) in and forward its forgery `(msg, encPair encUnary encBits (u, σ))` as `(u, msg, σ)`. -/ def counterForger (bound : ℕ → ℕ → ℕ) (adversary : Forger) : IndexedForger := fun n pk => do let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (S.counterHandler n bound)) (adversary n pk)).run 0 return ((requestDecoder.decode out.1.2).1, out.1.1, (requestDecoder.decode out.1.2).2) @@ -291,7 +291,7 @@ private noncomputable def jointOracle (n : ℕ) (sk : List Bool) (bound : ℕ (q : Unit × List Bool) (state : ℕ × List (ℕ × List Bool)) : PMF (List Bool × ℕ × List (ℕ × List Bool)) := ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.indexedSigningOracle n sk q s))) ((S.counterHandler n bound q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2)) @@ -329,11 +329,11 @@ private theorem map_run_jointOracle {n : ℕ} {sk : List Bool} {bound : ℕ → σ.length ≤ bound n msg.length) {α : Type} (program : WordOracleComp Unit α) : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (jointOracle S n sk bound)) program).run (0, [])).map (fun r => (r.1, r.2.1, r.2.2.map Prod.snd)) = ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.counterSigningOracle n sk)) program).run (0, [])) := by rw [ProbOracleComp.eval_run_interpret] refine ProbOracleComp.run_interpret_map_state_of_invariant _ _ @@ -376,7 +376,7 @@ private theorem eval_indexedEufCmaGame_counterForger (bound : ℕ → ℕ → ProbComp.eval (S.indexedEufCmaGame (S.counterForger bound adversary) n) = (ProbComp.eval (S.keyGen n)).bind fun keys => ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (jointOracle S n keys.2 bound)) (adversary n keys.1)).run (0, [])).map (indexedWin S keys.1) := by simp only [indexedEufCmaGame, counterForger, ProbComp.eval_bind, ProbComp.eval_pure, @@ -394,7 +394,7 @@ private theorem eval_counterEufCmaGame_eq {bound : ℕ → ℕ → ℕ} {n : ℕ ProbComp.eval (S.counterEufCmaGame adversary n) = (ProbComp.eval (S.keyGen n)).bind fun keys => ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (jointOracle S n keys.2 bound)) (adversary n keys.1)).run (0, [])).map (fun r => !(r.2.2.map Prod.snd).contains r.1.1 && S.counterVerify keys.1 r.1.1 r.1.2) := by @@ -474,12 +474,12 @@ private theorem counterHandler_bound {bound : ℕ → ℕ → ℕ} (c : ℕ × L (encUnary j).length + (bound c.1 request.2.length + 2 * S.capacity c.1 + 1) := by unfold counterHandler at hresult split_ifs at hresult with hj - · obtain ⟨sig, hsig, rfl⟩ := ProbOracleComp.mem_support_map hresult - obtain ⟨raw, -, rfl⟩ := ProbOracleComp.mem_support_map hsig + · obtain ⟨sig, hsig, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + obtain ⟨raw, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hsig have htake := List.length_take_le (bound c.1 request.2.length) raw simp only [length_encPair, encUnary_apply, encBits_apply, List.length_replicate] omega - · have h := ProbOracleComp.eq_of_mem_support_pure hresult + · have h := OracleComp.eq_of_mem_supportWith_pure hresult subst h simp only [List.length_nil, encUnary_apply, List.length_replicate] omega @@ -506,7 +506,7 @@ theorem isOraclePPT_counterForger {bound : ℕ → ℕ → ℕ} (encPair (encPair encBits encBits) encUnary) (fun c : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (S.counterHandler c.1 bound)) (adversary c.1 c.2)).run 0) := hadversary.run_interpret_preprocess_open' (prepare := fun c => c) diff --git a/Complexity/Crypto/Computational/MAC.lean b/Complexity/Crypto/Computational/MAC.lean index 5baba3606d..34d2a38b22 100644 --- a/Complexity/Crypto/Computational/MAC.lean +++ b/Complexity/Crypto/Computational/MAC.lean @@ -317,7 +317,7 @@ noncomputable def eufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) : ProbComp Bool := do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingOracle sk)) (adversary n [])).run [] return (out.1.1.length == M.msgLen n) && !out.2.contains out.1.1 && M.verify sk out.1.1 out.1.2 @@ -341,7 +341,7 @@ theorem isPPTOn_eufCmaGame (M : MACScheme) {adversary : Forger} (encPair (encPair encBits encBits) (encList encBits)) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingOracle caller.2)) (adversary caller.1 [])).run []) := by apply hadversary.run_interpret_preprocess (prepare := fun caller : ℕ × List Bool => (caller.1, ([] : List Bool))) @@ -421,7 +421,7 @@ noncomputable def eufOneTimeGame (M : MACScheme) (adversary : Forger) (n : ℕ) ProbComp Bool := do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningOracle sk)) (adversary n [])).run [] return (out.1.1.length == M.msgLen n) && !out.2.contains out.1.1 && M.verify sk out.1.1 out.1.2 @@ -435,7 +435,7 @@ theorem isPPTOn_run_oneTimeSigningOracle (M : MACScheme) {adversary : Forger} (encPair (encPair encBits encBits) (encList encBits)) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningOracle caller.2)) (adversary caller.1 [])).run []) := by obtain ⟨c, d, hlen⟩ := M.sign_ppt.length_le have hhandler : IsPPTOn @@ -522,15 +522,15 @@ private theorem run_limitToOneQuery_eq_oneTimeSigningOracle (M : MACScheme) tag.length ≤ bound n msg.length) (prog : WordOracleComp Unit (List Bool × List Bool)) : ProbComp.eval (Prod.map Prod.fst id <$> ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingOracle sk)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (SignatureScheme.oneTimeFilterHandler bound (n, []))) prog).run false)).run [])) = ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningOracle sk)) prog).run []) := by rw [ProbComp.eval_map, ProbOracleComp.eval_run_interpret, ProbOracleComp.eval_run_interpret, ProbOracleComp.run_interpret_run_interpret, PMF.map_comp] @@ -539,7 +539,7 @@ private theorem run_limitToOneQuery_eq_oneTimeSigningOracle (M : MACScheme) (oracle := fun q s => ProbComp.eval (M.oneTimeSigningOracle sk q s)) (oracle' := fun q (state : Bool × List (List Bool)) => ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (M.signingOracle sk q s))) ((SignatureScheme.oneTimeFilterHandler bound (n, []) q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -599,14 +599,14 @@ theorem EUFCMA.oneTimeEUFCMA {M : MACScheme} (h : M.EUFCMA) : M.OneTimeEUFCMA := have hrun := run_limitToOneQuery_eq_oneTimeSigningOracle M bound n sk htagBound (adversary n []) have hmap : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingOracle sk)) (SignatureScheme.limitToOneQuery bound adversary n [])).run []) = Prod.map Prod.fst id <$> ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingOracle sk)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (SignatureScheme.oneTimeFilterHandler bound (n, []))) (adversary n [])).run false)).run []) := by @@ -638,7 +638,7 @@ noncomputable def sufCmaGame (M : MACScheme) (adversary : Forger) (n : ℕ) : ProbComp Bool := do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) (adversary n [])).run [] return (out.1.1.length == M.msgLen n) && !out.2.contains out.1 && M.verify sk out.1.1 out.1.2 @@ -652,7 +652,7 @@ theorem isPPTOn_run_signingPairOracle (M : MACScheme) {adversary : Forger} (encPair (encPair encBits encBits) (encList (encPair encBits encBits))) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle caller.2)) (adversary caller.1 [])).run []) := by obtain ⟨c, d, hlen⟩ := M.sign_ppt.length_le have hhandler : IsPPTOn @@ -785,10 +785,10 @@ messages. -/ theorem eval_run_signingOracle_eq_map_fst_signingPairOracle (M : MACScheme) (sk : List Bool) (prog : WordOracleComp Unit (List Bool × List Bool)) : ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingOracle sk)) prog).run []) = (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) prog).run [])).map (fun (a, s') => (a, s'.map Prod.fst)) := by rw [ProbOracleComp.eval_run_interpret, ProbOracleComp.eval_run_interpret] @@ -809,7 +809,7 @@ theorem eval_eufCmaGame_eq_signingPairOracle (M : MACScheme) ProbComp.eval (do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) (adversary n [])).run [] return (out.1.1.length == M.msgLen n) && !(out.2.map Prod.fst).contains out.1.1 && M.verify sk out.1.1 out.1.2) := by @@ -872,7 +872,7 @@ private theorem mem_support_signingPairOracle (M : MACScheme) (sk : List Bool) (prog : WordOracleComp Unit (List Bool × List Bool)) (result : List Bool × List Bool) (queriedPairs : List (List Bool × List Bool)) (hmem : (result, queriedPairs) ∈ (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) prog).run [])).support) : ∀ pair ∈ queriedPairs, pair.2 ∈ (ProbComp.eval (M.sign sk pair.1)).support := by rw [ProbOracleComp.eval_run_interpret] at hmem @@ -974,7 +974,7 @@ noncomputable def sufOneTimeGame (M : MACScheme) (adversary : Forger) (n : ℕ) ProbComp Bool := do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningPairOracle sk)) (adversary n [])).run [] return (out.1.1.length == M.msgLen n) && !out.2.contains out.1 && M.verify sk out.1.1 out.1.2 @@ -988,7 +988,7 @@ theorem isPPTOn_run_oneTimeSigningPairOracle (M : MACScheme) {adversary : Forger (encPair (encPair encBits encBits) (encList (encPair encBits encBits))) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningPairOracle caller.2)) (adversary caller.1 [])).run []) := by obtain ⟨c, d, hlen⟩ := M.sign_ppt.length_le have hhandler : IsPPTOn @@ -1129,15 +1129,15 @@ private theorem run_limitToOneQuery_eq_oneTimeSigningPairOracle (M : MACScheme) tag.length ≤ bound n msg.length) (prog : WordOracleComp Unit (List Bool × List Bool)) : ProbComp.eval (Prod.map Prod.fst id <$> ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (SignatureScheme.oneTimeFilterHandler bound (n, []))) prog).run false)).run [])) = ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningPairOracle sk)) prog).run []) := by rw [ProbComp.eval_map, ProbOracleComp.eval_run_interpret, ProbOracleComp.eval_run_interpret, ProbOracleComp.run_interpret_run_interpret, PMF.map_comp] @@ -1145,7 +1145,7 @@ private theorem run_limitToOneQuery_eq_oneTimeSigningPairOracle (M : MACScheme) (oracle := fun q s => ProbComp.eval (M.oneTimeSigningPairOracle sk q s)) (oracle' := fun q (state : Bool × List (List Bool × List Bool)) => ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (M.signingPairOracle sk q s))) ((SignatureScheme.oneTimeFilterHandler bound (n, []) q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -1206,14 +1206,14 @@ theorem SUFCMA.oneTimeSUFCMA {M : MACScheme} (h : M.SUFCMA) : M.OneTimeSUFCMA := have hrun := run_limitToOneQuery_eq_oneTimeSigningPairOracle M bound n sk htagBound (adversary n []) have hmap : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) (SignatureScheme.limitToOneQuery bound adversary n [])).run []) = Prod.map Prod.fst id <$> ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (SignatureScheme.oneTimeFilterHandler bound (n, []))) (adversary n [])).run false)).run []) := by @@ -1231,10 +1231,10 @@ messages. -/ theorem eval_run_oneTimeSigningOracle_eq_map_fst_oneTimeSigningPairOracle (M : MACScheme) (sk : List Bool) (prog : WordOracleComp Unit (List Bool × List Bool)) : ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningOracle sk)) prog).run []) = (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningPairOracle sk)) prog).run [])).map (fun (a, s') => (a, s'.map Prod.fst)) := by rw [ProbOracleComp.eval_run_interpret, ProbOracleComp.eval_run_interpret] @@ -1257,7 +1257,7 @@ theorem eval_eufOneTimeGame_eq_oneTimeSigningPairOracle (M : MACScheme) ProbComp.eval (do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningPairOracle sk)) (adversary n [])).run [] return (out.1.1.length == M.msgLen n) && !(out.2.map Prod.fst).contains out.1.1 && M.verify sk out.1.1 out.1.2) := by @@ -1303,7 +1303,7 @@ private theorem mem_support_oneTimeSigningPairOracle (M : MACScheme) (sk : List (prog : WordOracleComp Unit (List Bool × List Bool)) (result : List Bool × List Bool) (queriedPairs : List (List Bool × List Bool)) (hmem : (result, queriedPairs) ∈ (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.oneTimeSigningPairOracle sk)) prog).run [])).support) : ∀ pair ∈ queriedPairs, pair.2 ∈ (ProbComp.eval (M.sign sk pair.1)).support := by rw [ProbOracleComp.eval_run_interpret] at hmem @@ -1620,7 +1620,7 @@ the PRF security game [Boneh and Shoup, Section 6.3, Theorem 6.2][BonehShoup2023 def macToPrfDistinguisher (adversary : Forger) : OracleDistinguisher := fun n _ => do let out ← (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (macLogHandler n)) (adversary n [])).run [] @@ -1652,7 +1652,7 @@ theorem isOraclePPT_macToPrfDistinguisher {adversary : Forger} (encPair (encPair encBits encBits) (encList encBits)) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (macLogHandler caller.1)) (adversary caller.1 [])).run []) := by @@ -1664,8 +1664,8 @@ theorem isOraclePPT_macToPrfDistinguisher {adversary : Forger} (fun _ _ => True) (fun _ => trivial) (by polytime) intro caller request queried _ result hresult unfold macLogHandler at hresult - obtain ⟨tag, htag, rfl⟩ := ProbOracleComp.mem_support_map hresult - obtain ⟨rawTag, _, rfl⟩ := ProbOracleComp.mem_support_map htag + obtain ⟨tag, htag, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + obtain ⟨rawTag, _, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp htag refine ⟨trivial, ?_, ?_⟩ · exact (List.length_take_le _ _).trans (by lia) · simp only [encList_cons, List.length_append, length_frame, encBits_apply] @@ -1701,20 +1701,20 @@ private theorem run_macLogHandler_eq_signingOracle (n : ℕ) (sk : List Bool) (hsk : sk.length = n) (prog : WordOracleComp Unit (List Bool × List Bool)) : ProbComp.eval (OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifFin (fun request => + (OracleComp.sumHandler ProbComp.unifFin (fun request => pure (prfOracle family n sk request.2))) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (macLogHandler n)) prog).run [])) = ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) ((prfMAC family hpoly).signingOracle sk)) prog).run []) := by have hread := ProbOracleComp.run_interpret_readOnly (fun request (_ : Unit) => PMF.pure (prfOracle family n sk request.2)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (macLogHandler n)) prog).run []) () @@ -1727,7 +1727,7 @@ private theorem run_macLogHandler_eq_signingOracle have hsim := ProbOracleComp.run_interpret_map_state (oracle := fun q (state : List (List Bool) × Unit) => ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun request (u : Unit) => (PMF.pure (prfOracle family n sk request.2)).map (·, u))) ((macLogHandler n q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -1737,7 +1737,7 @@ private theorem run_macLogHandler_eq_signingOracle intro ⟨⟨⟩, msg⟩ ⟨queried, ⟨⟩⟩ change PMF.map (fun (a, s') => (a, s'.1)) (((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun request (u : Unit) => (PMF.pure (prfOracle family n sk request.2)).map (·, u))) (macLogHandler n ((), msg) queried)).run ()).map (fun result => (result.1.1, result.1.2, result.2))) = @@ -1821,26 +1821,26 @@ theorem succProbability_prfIdealGame_macToPrfDistinguisher_le (adversary : Forge PMF (List Bool) := fun q state => ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun request => lazyRandomFunctionOracle n request.2)) ((macLogHandler n q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2)) let phase1 := ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) combinedOracle) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) combinedOracle) (adversary n [])).run ([], fun _ => none)) let phase2 : ((List Bool × List Bool) × List (List Bool) × RandomOracle.Cache (fun _ : BitString n => BitString n)) → PMF Bool := fun ⟨out, queried, cache⟩ => if (out.1.length == n) && !queried.contains out.1 then ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun request => lazyRandomFunctionOracle n request.2)) ((· == out.2) <$> (List.take n <$> ProbOracleComp.query ((), out.1)))).run cache).map Prod.fst else PMF.pure false have hgame : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun request => lazyRandomFunctionOracle n request.2)) (macToPrfDistinguisher adversary n [])).run (fun _ => none)).map Prod.fst = phase1.bind phase2 := by @@ -2297,7 +2297,7 @@ noncomputable def sufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) ( ProbComp Bool := do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) (adversary n [])).run [] return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) && decide (out.2.map (fun e => e.1.2)).Nodup && !out.2.contains out.1 && @@ -2310,7 +2310,7 @@ noncomputable def eufCmaGame (M : NonceMACScheme) (adversary : NonceMACForger) ( ProbComp Bool := do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) (adversary n [])).run [] return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) && decide (out.2.map (fun e => e.1.2)).Nodup && @@ -2327,7 +2327,7 @@ theorem isPPTOn_run_signingPairOracle (M : NonceMACScheme) {adversary : NonceMAC (encList (encPair (encPair encBits encBits) encBits))) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle caller.2)) (adversary caller.1 [])).run []) := by obtain ⟨c, d, hlen⟩ := M.sign_ppt.length_le have hhandler : IsPPTOn @@ -2549,7 +2549,7 @@ private theorem mem_support_signingPairOracle (M : NonceMACScheme) (sk : List Bo (result : (List Bool × List Bool) × List Bool) (queriedTriples : List ((List Bool × List Bool) × List Bool)) (hmem : (result, queriedTriples) ∈ (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) prog).run [])).support) : ∀ triple ∈ queriedTriples, triple.2 ∈ (ProbComp.eval (M.sign sk triple.1.1 triple.1.2)).support := by @@ -2584,7 +2584,7 @@ theorem eval_sufCmaGame_eq_freshPair_of_unique_tag (M : NonceMACScheme) ProbComp.eval (do let sk ← M.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (M.signingPairOracle sk)) (adversary n [])).run [] return (out.1.1.1.length == M.msgLen n) && (out.1.1.2.length == M.nonceLen n) && decide (out.2.map (fun e => e.1.2)).Nodup && diff --git a/Complexity/Crypto/Computational/MerkleSignature/Security.lean b/Complexity/Crypto/Computational/MerkleSignature/Security.lean index 3e4dae0a3b..5c1f715987 100644 --- a/Complexity/Crypto/Computational/MerkleSignature/Security.lean +++ b/Complexity/Crypto/Computational/MerkleSignature/Security.lean @@ -121,7 +121,7 @@ noncomputable def collisionFinder (adversary : IndexedForger) : CollisionFinder := fun n k => do let keys ← OracleComp.replicate (2 ^ depth n) (S.keyGen n) let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbComp.unifFin j)) + (OracleComp.sumHandler (fun j => StateT.lift (ProbComp.unifFin j)) ((scheme S H depth hH hlen hcap).indexedSigningOracle n (secretKey k keys))) (adversary n (publicKey H k keys))).run [] return collisionOf H k keys out @@ -163,7 +163,7 @@ noncomputable def oneTimeForgerAt (bound : ℕ → ℕ) (adversary : IndexedForg Forger := fun n vk => do let setup ← ProbOracleComp.sample (plantKeys S depth n i vk) let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j))) + (OracleComp.sumHandler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j))) (plantedHandler S H depth n setup.1 setup.2 i (bound n))) (adversary n (publicKey H setup.1 setup.2))).run [] return (H setup.1 out.1.2.1, (signatureDecoder.decode out.1.2.2).2.1) @@ -196,15 +196,15 @@ private theorem eval_run_plantedHandler σ.length ≤ b) {α : Type} (program : WordOracleComp Unit α) : (OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbComp.unifOracle j)) + (OracleComp.sumHandler (fun j => StateT.lift (ProbComp.unifOracle j)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle x.2 q s))) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j))) (plantedHandler S H depth n k (front ++ (x.1, []) :: back) front.length b)) program).run [])).run [] = (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbComp.unifFin j)) + (OracleComp.sumHandler (fun j => StateT.lift (ProbComp.unifFin j)) ((scheme S H depth hH hlen hcap).indexedSigningOracle n (secretKey k (front ++ x :: back)))) program).run [])).map (fun r => (r, otsLogOf H front.length k r.2)) := by @@ -215,7 +215,7 @@ private theorem eval_run_plantedHandler (secretKey k (front ++ x :: back)) q signed)) (oracle' := fun (q : Unit × List Bool) (state : List (ℕ × List Bool) × List (List Bool)) => ((OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbComp.unifOracle j)) + (OracleComp.sumHandler (fun j => StateT.lift (ProbComp.unifOracle j)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle x.2 q s))) ((plantedHandler S H depth n k (front ++ (x.1, []) :: back) front.length b q).run state.1)).run state.2).map @@ -229,7 +229,7 @@ private theorem eval_run_plantedHandler (pure a : StateT σ PMF β) state = PMF.pure (a, state) := fun _ _ => rfl have hsampleApply : ∀ {β : Type} (p : ProbComp β) (state : List (List Bool)), (OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbComp.unifOracle j)) + (OracleComp.sumHandler (fun j => StateT.lift (ProbComp.unifOracle j)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle x.2 q s))) (ProbOracleComp.sample p)) state = (ProbComp.eval p).map (·, state) := fun p state => ProbOracleComp.run_interpret_sample _ p state @@ -284,7 +284,7 @@ private noncomputable def realRun (adversary : IndexedForger) (n : ℕ) (k : List Bool) (keys : List (List Bool × List Bool)) : PMF ((ℕ × List Bool × List Bool) × List (ℕ × List Bool)) := ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbComp.unifFin j)) + (OracleComp.sumHandler (fun j => StateT.lift (ProbComp.unifFin j)) ((scheme S H depth hH hlen hcap).indexedSigningOracle n (secretKey k keys))) (adversary n (publicKey H k keys))).run []) @@ -653,7 +653,7 @@ theorem isPPT_collisionFinder {adversary : IndexedForger} (encPair (encPair encUnary (encPair encBits encBits)) (encList (encPair encUnary encBits))) (fun q : (ℕ × List Bool) × List (List Bool × List Bool) => (OracleComp.interpret - (ProbOracleComp.handler (fun j => StateT.lift (ProbComp.unifFin j)) + (OracleComp.sumHandler (fun j => StateT.lift (ProbComp.unifFin j)) ((scheme S H depth hH hlen hcap).indexedSigningOracle q.1.1 (secretKey q.1.2 q.2))) (adversary q.1.1 (publicKey H q.1.2 q.2))).run []) := hrun₀.preprocess (prepare := fun q : (ℕ × List Bool) × List (List Bool × List Bool) => @@ -901,8 +901,8 @@ private theorem plantedHandler_bound (hlen : ∀ k m, (H k m).length = k.length) unfold plantedHandler at hres dsimp only at hres split_ifs at hres with hguard hi - · obtain ⟨ots, hots, rfl⟩ := ProbOracleComp.mem_support_map hres - obtain ⟨raw, -, rfl⟩ := ProbOracleComp.mem_support_map hots + · obtain ⟨ots, hots, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hres + obtain ⟨raw, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hots have htake := List.length_take_le (bound n) raw have hvk := (hkeyLen i).1 have hp := hpath i @@ -912,10 +912,9 @@ private theorem plantedHandler_bound (hlen : ∀ k m, (H k m).length = k.length) · simp only [hdecode, encList_cons, encPair_apply, encUnary_apply, encBits_apply, List.length_append, length_frame, List.length_replicate] omega - · obtain ⟨sig, hsig, rfl⟩ := ProbOracleComp.mem_support_map hres - rw [ProbOracleComp.support_sample] at hsig - simp only [signWith, ProbComp.eval_bind, ProbComp.eval_pure, PMF.mem_support_bind_iff, - PMF.mem_support_pure_iff] at hsig + · obtain ⟨sig, hsig, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hres + simp only [ProbOracleComp.support_sample, signWith, ProbComp.eval_bind, ProbComp.eval_pure, + PMF.mem_support_bind_iff, PMF.mem_support_pure_iff] at hsig obtain ⟨ots, hots, rfl⟩ := hsig have hotsLen := hsignLen (_, _) ots hots simp only [encBits_apply, encPair_apply, List.length_append, length_frame, hlen] at hotsLen @@ -932,7 +931,7 @@ private theorem plantedHandler_bound (hlen : ∀ k m, (H k m).length = k.length) · simp only [hdecode, encList_cons, encPair_apply, encUnary_apply, encBits_apply, List.length_append, length_frame, List.length_replicate] omega - · have h := ProbOracleComp.eq_of_mem_support_pure hres + · have h := OracleComp.eq_of_mem_supportWith_pure hres subst h exact ⟨by simp, Nat.le_add_right _ _⟩ @@ -975,7 +974,7 @@ theorem isOraclePPT_oneTimeForger {bound : ℕ → ℕ} (encPair (encPair encUnary (encPair encBits encBits)) (encList (encPair encUnary encBits))) (fun c : ((ℕ × List Bool) × ℕ) × (List Bool × List (List Bool × List Bool)) => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j))) (plantedHandler S H depth c.1.1.1 c.2.1 c.2.2 c.1.2 (bound c.1.1.1))) (adversary c.1.1.1 (publicKey H c.2.1 c.2.2))).run []) := @@ -1017,7 +1016,7 @@ theorem isOraclePPT_oneTimeForger {bound : ℕ → ℕ} (second := fun (c : (ℕ × List Bool) × ℕ) (setup : List Bool × List (List Bool × List Bool)) => do let out ← (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun j => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin j))) (plantedHandler S H depth c.1.1 setup.1 setup.2 c.2 (bound c.1.1))) (adversary c.1.1 (publicKey H setup.1 setup.2))).run [] diff --git a/Complexity/Crypto/Computational/OneWay/MCSP.lean b/Complexity/Crypto/Computational/OneWay/MCSP.lean index 2a3d0937e7..9e3e4a268a 100644 --- a/Complexity/Crypto/Computational/OneWay/MCSP.lean +++ b/Complexity/Crypto/Computational/OneWay/MCSP.lean @@ -215,7 +215,7 @@ theorem tableInstance_map_tableQueries (oracle : List Bool → List Bool) (n m : /-- Against a deterministic oracle, the distinguisher runs the decider on the truth table of the oracle's restriction. -/ theorem interpret_mcspDistinguisher (d : ℕ) (oracle : List Bool → List Bool) (n : ℕ) : - OracleComp.interpret (ProbOracleComp.handler ProbComp.unifFin + OracleComp.interpret (OracleComp.sumHandler ProbComp.unifFin fun request => pure (oracle request.2)) (mcspDistinguisher p V d n []) = mcspRun p V ⟨tableArity d n, MCSP.truthTable (tableArity d n) (restriction oracle n (tableArity d n)), 2 ^ tableArity d n / (5 * tableArity d n)⟩ := by diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean index a3cc11acb0..a711b71689 100644 --- a/Complexity/Crypto/Computational/OneWayToSignature.lean +++ b/Complexity/Crypto/Computational/OneWayToSignature.lean @@ -581,7 +581,7 @@ noncomputable def lamportInverter (f : List Bool → List Bool) if j < 2 * n then do let keys ← lamportSimKeys f n j y let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) ((lamportScheme f hf).oneTimeSigningOracle keys.2)) (adversary n keys.1)).run [] return (frames out.1.2).getD (j / 2) [] else @@ -602,7 +602,7 @@ theorem isPPT_lamportInverter {f : List Bool → List Bool} encBits (fun r : ((ℕ × List Bool) × ℕ) × (List Bool × List Bool) => do let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) ((lamportScheme f (.of_tidy hf)).oneTimeSigningOracle r.2.2)) (adversary r.1.1.1 r.2.1)).run [] return (frames out.1.2).getD (r.1.2 / 2) []) := by @@ -645,7 +645,7 @@ theorem isPPT_lamportInverter {f : List Bool → List Bool} if q.2 < 2 * q.1.1 then do let keys ← lamportSimKeys f q.1.1 q.2 q.1.2 let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) ((lamportScheme f (.of_tidy hf)).oneTimeSigningOracle keys.2)) (adversary q.1.1 keys.1)).run [] return (frames out.1.2).getD (q.2 / 2) [] @@ -691,7 +691,7 @@ theorem OneWay.oneTimeEUFCMA_lamport {f : List Bool → List Bool} (hf : OneWay encList encBits (w.take j ++ [] :: w.drop (j + 1)) let runWith (pk sk : List Bool) : PMF ((List Bool × List Bool) × List (List Bool)) := ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.oneTimeSigningOracle sk)) (adversary n pk)).run []) let win (w : List (List Bool)) (out : (List Bool × List Bool) × List (List Bool)) : Bool := (out.1.1.length == n) && !out.2.contains out.1.1 && @@ -703,7 +703,7 @@ theorem OneWay.oneTimeEUFCMA_lamport {f : List Bool → List Bool} (hf : OneWay if j < 2 * n then do let keys ← lamportSimKeys f n j y let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.oneTimeSigningOracle keys.2)) (adversary n keys.1)).run [] return (frames out.1.2).getD (j / 2) [] else diff --git a/Complexity/Crypto/Computational/PseudorandomFunction.lean b/Complexity/Crypto/Computational/PseudorandomFunction.lean index 9c126aca71..23987227f1 100644 --- a/Complexity/Crypto/Computational/PseudorandomFunction.lean +++ b/Complexity/Crypto/Computational/PseudorandomFunction.lean @@ -76,7 +76,7 @@ def randomFunctionQuery (n : ℕ) (query : List Bool) : theorem interpret_randomFunctionQuery {m : Type → Type*} [Monad m] [LawfulMonad m] (random : (n : ℕ) → m (Fin (n + 1))) (n : ℕ) (table : BitString n → BitString n) (query : List Bool) : - OracleComp.interpret (ProbOracleComp.handler random (fun bits => pure (table bits))) + OracleComp.interpret (OracleComp.sumHandler random (fun bits => pure (table bits))) (randomFunctionQuery n query) = pure (randomFunctionOracle n table query) := by by_cases h : query.length = n <;> simp [randomFunctionQuery, randomFunctionOracle, h] @@ -85,7 +85,7 @@ open Classical in noncomputable def lazyRandomFunctionOracle (n : ℕ) (query : List Bool) : StateT (RandomOracle.Cache (fun _ : BitString n => BitString n)) PMF (List Bool) := OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (RandomOracle.answer (fun _ => PMF.uniformOfFintype (BitString n)))) (randomFunctionQuery n query) @@ -94,14 +94,14 @@ noncomputable def prfRealGame (family : List Bool → List Bool → List Bool) (adversary : OracleDistinguisher) (n : ℕ) : ProbComp Bool := do let key ← BitString.sampleList n OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifFin (fun request => + (OracleComp.sumHandler ProbComp.unifFin (fun request => pure (prfOracle family n key request.2))) (adversary n []) /-- Sample one whole random function, independently of the adversary's private samples. -/ noncomputable def prfIdealGame (adversary : OracleDistinguisher) (n : ℕ) : ProbComp Bool := do let table ← ProbComp.uniform (BitString n → BitString n) OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifFin (fun request => + (OracleComp.sumHandler ProbComp.unifFin (fun request => pure (randomFunctionOracle n table request.2))) (adversary n []) /-- The ideal game admits consistent lazy answers to adaptive queries, with private randomness @@ -109,17 +109,17 @@ independent of the table and the same rejection convention for malformed inputs. theorem prfIdealGame_eq_lazy (adversary : OracleDistinguisher) (n : ℕ) : ProbComp.eval (prfIdealGame adversary n) = ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun request => lazyRandomFunctionOracle n request.2)) (adversary n [])).run (fun _ => none)).map Prod.fst := by classical let adapted := OracleComp.interpret - (ProbOracleComp.handler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) (fun request : Unit × List Bool => randomFunctionQuery n request.2)) (adversary n []) have h := RandomOracle.uniform_interpret_prob_eq_lazy adapted have heager (table : BitString n → BitString n) (query : List Bool) : OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifOracle (fun bits => PMF.pure (table bits))) + (OracleComp.sumHandler ProbComp.unifOracle (fun bits => PMF.pure (table bits))) (randomFunctionQuery n query) = PMF.pure (randomFunctionOracle n table query) := interpret_randomFunctionQuery ProbComp.unifOracle n table query simpa only [adapted, prfIdealGame, ProbComp.eval_bind, ProbComp.eval_uniform, diff --git a/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean b/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean index facd02145a..f031b0d3ba 100644 --- a/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean +++ b/Complexity/Crypto/Computational/PseudorandomFunction/Coins.lean @@ -144,7 +144,7 @@ def randomCoinOracle (N : ℕ) (table : BitString N → BitString N) (request : noncomputable def coinRealGame (adversary : OracleDistinguisher) (N : ℕ) : ProbComp Bool := do let key ← BitString.sampleList N OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifFin (fun request => + (OracleComp.sumHandler ProbComp.unifFin (fun request => pure (coinOracle family key request.2))) (adversary N []) /-- The ideal coin game: a uniform random function on `N` bits answers every request at its @@ -152,7 +152,7 @@ padding, cut to the requested count. -/ noncomputable def coinIdealGame (adversary : OracleDistinguisher) (N : ℕ) : ProbComp Bool := do let table ← ProbComp.uniform (BitString N → BitString N) OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifFin (fun request => + (OracleComp.sumHandler ProbComp.unifFin (fun request => pure (randomCoinOracle N table request.2))) (adversary N []) /-! ### The reduction to the PRF games -/ @@ -165,16 +165,16 @@ def coinQuery (N : ℕ) (request : Unit × List Bool) : WordOracleComp Unit (Lis /-- The PRF distinguisher built from a coin adversary: run it, answering through `coinQuery`. -/ def coinDistinguisher (adversary : OracleDistinguisher) : OracleDistinguisher := fun N aux => OracleComp.interpret - (ProbOracleComp.handler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) (coinQuery N)) + (OracleComp.sumHandler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) (coinQuery N)) (adversary N aux) /-- Interpreting the forwarded program against a stateless word oracle is interpreting the original program against that oracle composed with `coinQuery`. -/ private theorem interpret_coinDistinguisher (oracle : Unit × List Bool → ProbComp (List Bool)) (adversary : OracleDistinguisher) (N : ℕ) (aux : List Bool) : - OracleComp.interpret (ProbOracleComp.handler ProbComp.unifFin oracle) + OracleComp.interpret (OracleComp.sumHandler ProbComp.unifFin oracle) (coinDistinguisher adversary N aux) = - OracleComp.interpret (ProbOracleComp.handler ProbComp.unifFin (fun request => + OracleComp.interpret (OracleComp.sumHandler ProbComp.unifFin (fun request => List.take (coinRequestDecoder.decode request.2).2 <$> oracle ((), padRequest N (coinRequestDecoder.decode request.2).1))) (adversary N aux) := by simp only [coinDistinguisher, OracleComp.interpret_interpret, OracleComp.interpret_sumHandler, @@ -191,7 +191,7 @@ theorem eval_coinRealGame (adversary : OracleDistinguisher) (N : ℕ) : have hlen := BitString.length_of_mem_support_uniformList hkey rw [interpret_coinDistinguisher] refine congrArg (fun h => ProbComp.eval (OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifFin h) (adversary N []))) (funext fun request => ?_) + (OracleComp.sumHandler ProbComp.unifFin h) (adversary N []))) (funext fun request => ?_) simp only [map_pure, coinOracle, prfCoins, prfOracle, length_padRequest, hlen, ite_true] /-- The ideal coin game is the ideal PRF game of the forwarded adversary. -/ @@ -202,7 +202,7 @@ theorem eval_coinIdealGame (adversary : OracleDistinguisher) (N : ℕ) : refine PMF.bind_congr_on_support _ _ _ fun table _ => ?_ rw [interpret_coinDistinguisher] refine congrArg (fun h => ProbComp.eval (OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifFin h) (adversary N []))) (funext fun request => ?_) + (OracleComp.sumHandler ProbComp.unifFin h) (adversary N []))) (funext fun request => ?_) simp only [map_pure, randomCoinOracle] /-- `coinQuery` as a handler with trivial state, for the open substitution rule. -/ @@ -244,10 +244,10 @@ theorem isOraclePPT_coinDistinguisher {adversary : OracleDistinguisher} (fun _ => trivial) (by polytime) ?_ · refine (hrun.map' (ComputableInPolyTime.fst encBool (encFinEnum Unit))).congr fun c External oracle e => ?_ - have hlift : ProbOracleComp.handler + have hlift : OracleComp.sumHandler (fun n => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin n))) (fun q => coinHandler c.1 q) = - fun q => StateT.lift (σ := Unit) (ProbOracleComp.handler + fun q => StateT.lift (σ := Unit) (OracleComp.sumHandler (fun n => ProbOracleComp.sample (ProbComp.unifFin n)) (coinQuery c.1) q) := by funext q cases q with @@ -256,7 +256,7 @@ theorem isOraclePPT_coinDistinguisher {adversary : OracleDistinguisher} funext u exact map_eq_pure_bind _ _ have h : Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun n => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin n))) (fun q => coinHandler c.1 q)) (adversary c.1 c.2)).run () = coinDistinguisher adversary c.1 c.2 := by @@ -264,8 +264,8 @@ theorem isOraclePPT_coinDistinguisher {adversary : OracleDistinguisher} exact id_map _ rw [h] · intro c request u _ result hresult - obtain ⟨reply, hreply, rfl⟩ := ProbOracleComp.mem_support_map hresult - obtain ⟨raw, -, rfl⟩ := ProbOracleComp.mem_support_map hreply + obtain ⟨reply, hreply, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + obtain ⟨raw, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hreply refine ⟨trivial, (List.length_take_le _ _).trans ?_, le_add_right le_rfl⟩ exact length_dropFrame_le request.2 diff --git a/Complexity/Crypto/Computational/PseudorandomFunction/RandomOracle.lean b/Complexity/Crypto/Computational/PseudorandomFunction/RandomOracle.lean index 5ae322a8ac..49847f8910 100644 --- a/Complexity/Crypto/Computational/PseudorandomFunction/RandomOracle.lean +++ b/Complexity/Crypto/Computational/PseudorandomFunction/RandomOracle.lean @@ -74,7 +74,7 @@ consistency and independent private randomness under arbitrary adaptive interact theorem prfIdealGame_eq_cached (adversary : OracleDistinguisher) (n : ℕ) : ProbComp.eval (prfIdealGame adversary n) = ProbComp.eval (Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (fun request => cachedRandomFunctionOracle n request.2)) (adversary n [])).run []) := by let adapter := fun query : List Bool => if query.length = n then (ProbOracleComp.query (BitString.ofList n query) : @@ -84,10 +84,10 @@ theorem prfIdealGame_eq_cached (adversary : OracleDistinguisher) (n : ℕ) : (⟨List.ofFn, List.ofFn_injective⟩ : BitString n ↪ List Bool) List.ofFn (fun _ => PMF.uniformOfFintype (BitString n)) (fun _ => BitString.uniformList n) (fun _ => rfl) (OracleComp.interpret - (ProbOracleComp.handler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => ProbOracleComp.sample (ProbComp.unifFin k)) (fun request : Unit × List Bool => adapter request.2)) (adversary n [])) have hstep (query : List Bool) : OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun key => memoize (fun _ => BitString.uniformList n) (List.ofFn key))) (adapter query) = fun cache => ProbComp.eval (cachedRandomFunctionOracle n query cache) := by @@ -99,7 +99,7 @@ theorem prfIdealGame_eq_cached (adversary : OracleDistinguisher) (n : ℕ) : OracleComp.interpret_pure, ProbComp.eval_pure] rfl have heager (table : BitString n → BitString n) (query : List Bool) : OracleComp.interpret - (ProbOracleComp.handler ProbComp.unifOracle (fun key => PMF.pure (List.ofFn (table key)))) + (OracleComp.sumHandler ProbComp.unifOracle (fun key => PMF.pure (List.ofFn (table key)))) (adapter query) = PMF.pure (randomFunctionOracle n table query) := by by_cases hquery : query.length = n <;> simp [adapter, randomFunctionOracle, hquery] rw [ProbComp.eval_map, ProbOracleComp.eval_run_interpret] @@ -118,7 +118,7 @@ theorem isPPT_prfIdealGame {adversary : OracleDistinguisher} have hrun : IsPPTOn (encPair encUnary encBits) (encPair encBool (encList (encPair encBits encBits))) (fun pair : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (fun request => cachedRandomFunctionOracle pair.1 request.2)) (adversary pair.1 [])).run []) := by apply hadversary.run_interpret_preprocess (operationEncoding := encFinEnum Unit) diff --git a/Complexity/Crypto/Computational/PseudorandomFunction/TruthTable.lean b/Complexity/Crypto/Computational/PseudorandomFunction/TruthTable.lean index 0393b9f4c6..f73c366355 100644 --- a/Complexity/Crypto/Computational/PseudorandomFunction/TruthTable.lean +++ b/Complexity/Crypto/Computational/PseudorandomFunction/TruthTable.lean @@ -109,11 +109,11 @@ theorem isOraclePPTOn_queryTable : IsOraclePPTOn (encList encBits) encBits query cases words with | nil => simp only [queryTableStep, List.isEmpty_nil, ite_true] at hnext - rw [ProbOracleComp.eq_of_mem_support_pure hnext] + rw [OracleComp.eq_of_mem_supportWith_pure hnext] simp | cons word words => simp only [queryTableStep, List.isEmpty_cons, Bool.false_eq_true, ite_false] at hnext - obtain ⟨reply, -, rfl⟩ := ProbOracleComp.mem_support_map hnext + obtain ⟨reply, -, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hnext simp only [length_encPair, encBits_apply, List.length_append, List.length_singleton, List.tail_cons, length_encList, List.map_cons, List.sum_cons] omega @@ -122,10 +122,10 @@ theorem isOraclePPTOn_queryTable : IsOraclePPTOn (encList encBits) encBits query theorem interpret_queryTable {m : Type → Type*} [Monad m] [LawfulMonad m] (random : (n : ℕ) → m (Fin (n + 1))) (oracle : List Bool → List Bool) (words : List (List Bool)) : - OracleComp.interpret (ProbOracleComp.handler random fun request => pure (oracle request.2)) + OracleComp.interpret (OracleComp.sumHandler random fun request => pure (oracle request.2)) (queryTable words) = pure (words.map fun word => (oracle word).headD false) := by have key : ∀ (words : List (List Bool)) (acc : List Bool), - OracleComp.interpret (ProbOracleComp.handler random fun request => pure (oracle request.2)) + OracleComp.interpret (OracleComp.sumHandler random fun request => pure (oracle request.2)) (OracleComp.iterate words.length queryTableStep (words, acc)) = pure ([], acc ++ words.map fun word => (oracle word).headD false) := by intro words @@ -135,7 +135,7 @@ theorem interpret_queryTable {m : Type → Type*} [Monad m] [LawfulMonad m] intro acc rw [List.length_cons, OracleComp.iterate_succ_bind, OracleComp.interpret_bind] have hstep : OracleComp.interpret - (ProbOracleComp.handler random fun request => pure (oracle request.2)) + (OracleComp.sumHandler random fun request => pure (oracle request.2)) (queryTableStep (word :: words, acc)) = pure (words, acc ++ [(oracle word).headD false]) := by simp only [queryTableStep, List.isEmpty_cons, Bool.false_eq_true, ite_false, diff --git a/Complexity/Crypto/Computational/Signature.lean b/Complexity/Crypto/Computational/Signature.lean index 204b91866f..9a46e6a270 100644 --- a/Complexity/Crypto/Computational/Signature.lean +++ b/Complexity/Crypto/Computational/Signature.lean @@ -171,7 +171,7 @@ def eufCmaGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) : ProbComp Bool := do let keys ← S.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.signingOracle keys.2)) (adversary n keys.1)).run [] return (out.1.1.length == n) && !out.2.contains out.1.1 && S.verify keys.1 out.1.1 out.1.2 @@ -196,7 +196,7 @@ theorem isPPTOn_eufCmaGame (S : SignatureScheme) {adversary : Forger} (encPair (encPair encBits encBits) (encList encBits)) (fun caller : ℕ × (List Bool × List Bool) => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.signingOracle caller.2.2)) (adversary caller.1 caller.2.1)).run []) := by apply hadversary.run_interpret_preprocess (prepare := fun caller : ℕ × (List Bool × List Bool) => (caller.1, caller.2.1)) @@ -273,7 +273,7 @@ def eufOneTimeGame (S : SignatureScheme) (adversary : Forger) (n : ℕ) : ProbComp Bool := do let keys ← S.keyGen n let out ← (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.oneTimeSigningOracle keys.2)) (adversary n keys.1)).run [] return (out.1.1.length == n) && !out.2.contains out.1.1 && S.verify keys.1 out.1.1 out.1.2 @@ -287,7 +287,7 @@ theorem isPPTOn_run_oneTimeSigningOracle (S : SignatureScheme) {adversary : Forg (encPair (encPair encBits encBits) (encList encBits)) (fun caller : ℕ × (List Bool × List Bool) => (OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.oneTimeSigningOracle caller.2.2)) (adversary caller.1 caller.2.1)).run []) := by obtain ⟨c, d, hlen⟩ := S.sign_ppt.length_le have hhandler : IsPPTOn @@ -375,7 +375,7 @@ message. -/ theorem length_le_one_of_mem_support_run_oneTimeSigningOracle (S : SignatureScheme) {α : Type} (sk : List Bool) (prog : WordOracleComp Unit α) {result : α} {queried : List (List Bool)} (h : (result, queried) ∈ ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle sk q s))) prog).run []).support) : queried.length ≤ 1 := by refine ProbOracleComp.run_interpret_invariant @@ -398,7 +398,7 @@ private theorem run_oneTimeSigningOracle_apply_eq_zero_of_not_agree (S : Signatu {s queried' : List (List Bool)} (hs : ¬ ∀ r ∈ s, agree r) (hq' : ∀ r ∈ queried', agree r) (a : α) : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle sk q s))) prog).run s) (a, queried') = 0 := by rw [PMF.apply_eq_zero_iff] @@ -427,10 +427,10 @@ theorem run_oneTimeSigningOracle_apply_eq_of_agree (S : SignatureScheme) {α : T (prog : WordOracleComp Unit α) (s : List (List Bool)) (a : α) (queried' : List (List Bool)) (hq' : ∀ r ∈ queried', agree r) : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle sk₁ q s))) prog).run s) (a, queried') = ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle sk₂ q s))) prog).run s) (a, queried') := by induction prog using PFunctor.FreeM.induction generalizing s with @@ -464,13 +464,13 @@ theorem run_oneTimeSigningOracle_apply_eq_of_agree (S : SignatureScheme) {α : T PMF.bind_apply] have h1 (sig : List Bool) : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle sk₁ q s))) (cont sig)).run [msg]) (a, queried') = 0 := run_oneTimeSigningOracle_apply_eq_zero_of_not_agree S sk₁ (cont sig) hnot hq' a have h2 (sig : List Bool) : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.oneTimeSigningOracle sk₂ q s))) (cont sig)).run [msg]) (a, queried') = 0 := run_oneTimeSigningOracle_apply_eq_zero_of_not_agree S sk₂ (cont sig) hnot hq' a @@ -495,7 +495,7 @@ def oneTimeFilterHandler (bound : ℕ → ℕ → ℕ) (caller : ℕ × List Boo def limitToOneQuery (bound : ℕ → ℕ → ℕ) (adversary : Forger) : Forger := fun n pk => Prod.fst <$> (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (oneTimeFilterHandler bound (n, pk))) (adversary n pk)).run false @@ -547,7 +547,7 @@ theorem isOraclePPT_limitToOneQuery {bound : ℕ → ℕ → ℕ} (encPair (encPair encBits encBits) encBool) (fun caller : ℕ × List Bool => (OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (oneTimeFilterHandler bound caller)) (adversary caller.1 caller.2)).run false) := by @@ -568,11 +568,11 @@ theorem isOraclePPT_limitToOneQuery {bound : ℕ → ℕ → ℕ} intro caller request state _ result hresult unfold oneTimeFilterHandler at hresult split_ifs at hresult with hstate - · have heq := ProbOracleComp.eq_of_mem_support_pure hresult + · have heq := OracleComp.eq_of_mem_supportWith_pure hresult subst heq simp [encBool_apply] - · obtain ⟨sig, hsig, rfl⟩ := ProbOracleComp.mem_support_map hresult - obtain ⟨rawSig, _, rfl⟩ := ProbOracleComp.mem_support_map hsig + · obtain ⟨sig, hsig, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hresult + obtain ⟨rawSig, _, rfl⟩ := OracleComp.mem_supportWith_map_iff.mp hsig refine ⟨trivial, ?_, ?_⟩ · exact (List.length_take_le _ _).trans (by lia) · simp [encBool_apply] @@ -585,15 +585,15 @@ private theorem run_limitToOneQuery_eq_oneTimeSigningOracle (S : SignatureScheme sig.length ≤ bound n msg.length) (prog : WordOracleComp Unit (List Bool × List Bool)) : ProbComp.eval (Prod.map Prod.fst id <$> ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.signingOracle sk)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (oneTimeFilterHandler bound (n, pk))) prog).run false)).run [])) = ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.oneTimeSigningOracle sk)) prog).run []) := by rw [ProbComp.eval_map, ProbOracleComp.eval_run_interpret, ProbOracleComp.eval_run_interpret, ProbOracleComp.run_interpret_run_interpret, PMF.map_comp] @@ -602,7 +602,7 @@ private theorem run_limitToOneQuery_eq_oneTimeSigningOracle (S : SignatureScheme (oracle := fun q s => ProbComp.eval (S.oneTimeSigningOracle sk q s)) (oracle' := fun q (state : Bool × List (List Bool)) => ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifOracle k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifOracle k)) (fun q s => ProbComp.eval (S.signingOracle sk q s))) ((oneTimeFilterHandler bound (n, pk) q).run state.1)).run state.2).map (fun result => (result.1.1, result.1.2, result.2))) @@ -662,14 +662,14 @@ theorem EUFCMA.oneTimeEUFCMA {S : SignatureScheme} (h : S.EUFCMA) : S.OneTimeEUF have hrun := run_limitToOneQuery_eq_oneTimeSigningOracle S bound n keys.1 keys.2 hsigBound (adversary n keys.1) have hmap : ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.signingOracle keys.2)) (limitToOneQuery bound adversary n keys.1)).run []) = Prod.map Prod.fst id <$> ((OracleComp.interpret - (ProbOracleComp.handler (fun k => StateT.lift (ProbComp.unifFin k)) + (OracleComp.sumHandler (fun k => StateT.lift (ProbComp.unifFin k)) (S.signingOracle keys.2)) ((OracleComp.interpret - (ProbOracleComp.handler + (OracleComp.sumHandler (fun k => StateT.lift (ProbOracleComp.sample (ProbComp.unifFin k))) (oneTimeFilterHandler bound (n, keys.1))) (adversary n keys.1)).run false)).run []) := by diff --git a/Complexity/Crypto/Game/UntilBad.lean b/Complexity/Crypto/Game/UntilBad.lean index f80d1e46db..935d7daf50 100644 --- a/Complexity/Crypto/Game/UntilBad.lean +++ b/Complexity/Crypto/Game/UntilBad.lean @@ -93,7 +93,7 @@ open scoped ENNReal NNReal noncomputable def runStatelessOracle {α : Type} (o : List Bool → List Bool) (prog : WordOracleComp Unit α) (next : α → Game) : Game := (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (fun req (s : Unit) => pure (o req.2, s))) prog).run ())).bind (fun out => next out.1) @@ -111,7 +111,7 @@ theorem runStatelessOracle_query_inl {α : Type} (o : List Bool → List Bool) runStatelessOracle o (OracleComp.query (Sum.inl m) >>= k) next = (PMF.uniformOfFintype (Fin (m + 1))).bind (fun x => runStatelessOracle o (k x) next) := by - simp [runStatelessOracle, ProbOracleComp.handler, StateT.run_bind, + simp [runStatelessOracle, OracleComp.sumHandler, StateT.run_bind, ProbComp.eval_bind, PMF.bind_bind] theorem runStatelessOracle_query_inr {α : Type} (o : List Bool → List Bool) @@ -122,7 +122,7 @@ theorem runStatelessOracle_query_inr {α : Type} (o : List Bool → List Bool) runStatelessOracle o (OracleComp.query (Sum.inr req) >>= k) next = runStatelessOracle o (k (o req.2)) next := by rw [runStatelessOracle, OracleComp.interpret_bind, OracleComp.interpret_query, - ProbOracleComp.handler, StateT.run_bind] + OracleComp.sumHandler, StateT.run_bind] rfl /-- **Stateless oracle until-bad bound**: if `prog` makes at most `Q` oracle queries, `o₁ τ req` @@ -239,7 +239,7 @@ theorem advantage_runStatelessOracle_le_of_support {α : Type} (o : List Bool → List Bool) (prog : WordOracleComp Unit α) (next₁ next₂ : α → Game) {ε : ℝ≥0} (h : ∀ out ∈ (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (fun req (s : Unit) => pure (o req.2, s))) prog).run ())).support, Game.advantage (next₁ out.1) (next₂ out.1) ≤ ε) : Game.advantage (runStatelessOracle o prog next₁) (runStatelessOracle o prog next₂) ≤ ε := @@ -282,7 +282,7 @@ noncomputable def runFinderOracle {α : Type} (o₂ : List Bool → List Bool) (prog : WordOracleComp Unit α) (s : Option (List Bool)) (isGood : List Bool → Bool) : Game := (ProbComp.eval ((OracleComp.interpret - (ProbOracleComp.handler (fun m => StateT.lift (ProbComp.unifFin m)) + (OracleComp.sumHandler (fun m => StateT.lift (ProbComp.unifFin m)) (finderPhase2Oracle o₂ isBad extract)) prog).run s)).bind (fun out => PMF.pure (out.2.elim false isGood)) @@ -302,7 +302,7 @@ theorem runFinderOracle_query_inl {α : Type} (o₂ : List Bool → List Bool) runFinderOracle o₂ isBad extract (OracleComp.query (Sum.inl m) >>= k) s isGood = (PMF.uniformOfFintype (Fin (m + 1))).bind (fun x => runFinderOracle o₂ isBad extract (k x) s isGood) := by - simp [runFinderOracle, ProbOracleComp.handler, StateT.run_bind, + simp [runFinderOracle, OracleComp.sumHandler, StateT.run_bind, ProbComp.eval_bind, PMF.bind_bind] theorem runFinderOracle_query_inr {α : Type} (o₂ : List Bool → List Bool) @@ -315,7 +315,7 @@ theorem runFinderOracle_query_inr {α : Type} (o₂ : List Bool → List Bool) runFinderOracle o₂ isBad extract (k (o₂ req.2)) (if isBad req.2 then some (extract req.2) else s) isGood := by rw [runFinderOracle, OracleComp.interpret_bind, OracleComp.interpret_query, - ProbOracleComp.handler, StateT.run_bind] + OracleComp.sumHandler_inr, StateT.run_bind] rfl /-- Once `s` satisfies `s.elim false isGood = true`, `runFinderOracle` succeeds with diff --git a/Complexity/Languages/Probabilistic/Oracle.lean b/Complexity/Languages/Probabilistic/Oracle.lean index 8a5b4e9c19..f0ff953b8c 100644 --- a/Complexity/Languages/Probabilistic/Oracle.lean +++ b/Complexity/Languages/Probabilistic/Oracle.lean @@ -89,13 +89,6 @@ theorem isMonadHom_sample : IsMonadHom ProbComp (ProbOracleComp spec) (sample (s /-- Make one external call, whose reply may determine later sampling or queries. -/ def query (q : Query) : ProbOracleComp spec (spec q) := OracleComp.query (Sum.inr q) -/-- Transitional name for the sum handler `OracleComp.sumHandler` of `unifSpec ⊕ₒ spec`, kept -only until its remaining clients use `OracleComp.sumHandler` directly (#814). -/ -abbrev handler {m : Type → Type v} (random : (n : ℕ) → m (Fin (n + 1))) - (oracle : (q : Query) → m (spec q)) : - (q : ℕ ⊕ Query) → m (probOracleSpec spec q) := - OracleComp.sumHandler random oracle - open OracleComp (sumHandler) variable {m : Type → Type v} [Monad m] [LawfulMonad m] diff --git a/Complexity/Languages/Probabilistic/Oracle/Support.lean b/Complexity/Languages/Probabilistic/Oracle/Support.lean index 3b69caf5c6..f8c0ad7421 100644 --- a/Complexity/Languages/Probabilistic/Oracle/Support.lean +++ b/Complexity/Languages/Probabilistic/Oracle/Support.lean @@ -51,16 +51,6 @@ open OracleComp variable {Query α β : Type} {spec : Query → Type} -/-- A returned value is the only possible result. -/ -theorem eq_of_mem_support_pure {a result : α} - (h : result ∈ support (pure a : ProbOracleComp spec α)) : result = a := - eq_of_mem_supportWith_pure h - -/-- A possible mapped result is the image of a possible result. -/ -theorem mem_support_map {program : ProbOracleComp spec α} {f : α → β} {result : β} - (h : result ∈ support (f <$> program)) : ∃ a ∈ support program, f a = result := - mem_supportWith_map_iff.mp h - /-- An external query may return any of its possible replies. -/ @[simp] theorem supportWith_query (possible : (q : ℕ ⊕ Query) → Set (probOracleSpec spec q)) (q : Query) : supportWith possible (query (spec := spec) q) = possible (.inr q) :=