diff --git a/Complexity.lean b/Complexity.lean index dfa9144bae..cf733f246b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1812,6 +1812,7 @@ public import Complexity.Languages.Probabilistic.Presample public import Complexity.Languages.Probabilistic.QueryCount public import Complexity.Languages.Probabilistic.RandomOracle public import Complexity.Languages.Probabilistic.RandomOracle.Probabilistic +public import Complexity.Languages.Probabilistic.RandomPermutation public import Complexity.Languages.Probabilistic.Repeat public import Complexity.Languages.Probabilistic.Selection public import Complexity.Languages.Probabilistic.Semantics diff --git a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean index 2b27e3d899..f168e5f118 100644 --- a/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean +++ b/Complexity/Crypto/Protocols/Cipher/EvenMansour.lean @@ -10,8 +10,10 @@ module public import Complexity.Crypto.Game public import Complexity.Foundations.Data.BitString.Basic public import Complexity.Languages.Probabilistic.QueryCount +public import Complexity.Languages.Probabilistic.RandomPermutation public import Complexity.Languages.Probabilistic.Sum public import Mathlib.Data.Fintype.Perm +import Complexity.Languages.Probabilistic.Simulation import Complexity.Probability.BitString import Complexity.Probability.PMF.Bind import Complexity.Probability.PMF.Uniform @@ -42,12 +44,14 @@ We formalize four aspects of the Even–Mansour construction: query, `IsCallBounded _ 1 1`) to recover the secret key with probability `1` and achieve key-recovery game advantage `1 - |G|⁻¹` against an independent uniform permutation and uniform target key (`advantage_preWhitenKeyRecoveryGame_eq`, `advantage_postWhitenKeyRecoveryGame_eq`). -3. **One-sided query security**: because `evenMansourPermEquiv k₀ k₁` is a bijection on - `Equiv.Perm G`, any adversary that queries only the cipher oracle (`liftLeft`) or only the - primitive permutation oracle (`liftRight`) has zero distinguishing advantage between the real - Even–Mansour game and two independent uniform permutations - (`advantage_evenMansourRealGame_liftLeft_eq_zero`, - `advantage_evenMansourRealGame_liftRight_eq_zero`). +3. **One-sided query security and lazy ideal-permutation equivalence**: because + `evenMansourPermEquiv k₀ k₁` is a bijection on `Equiv.Perm G`, any adversary that queries only + the cipher oracle (`liftLeft`) or only the primitive permutation oracle (`liftRight`) has zero + distinguishing advantage between the real Even–Mansour game and two independent uniform + permutations (`advantage_evenMansourRealGame_liftLeft_eq_zero`, + `advantage_evenMansourRealGame_liftRight_eq_zero`). Moreover, `evenMansourIdealGame` is + identically distributed to running two independent lazy bidirectional permutation samplers + (`idealLazyHandler`) from empty caches (`evenMansourIdealGame_eq_lazy`). 4. **Bad-key transcript intersection bound ([BonehShoup2023], Theorem 4.10)**: given a cipher transcript `T_e : List (G × G)` and a primitive permutation transcript `T_π : List (G × G)`, a key `(k₀, k₁)` is bad (`isBadEvenMansourKey T_e T_π k`) when some `(x, y) ∈ T_e` and @@ -63,9 +67,10 @@ We formalize four aspects of the Even–Mansour construction: `IsCallBounded program Q_e Q_π`, `OracleComp.IsCostBounded.transcript_cost_le` bounds every supported transcript by `|T_e| ≤ Q_e` and `|T_π| ≤ Q_π`, yielding the `2 * Q_e * Q_π / |G|` bad-key bound on every supported execution path (`IsCallBounded.badEvenMansourKey_toReal_le`, - `IsCallBounded.badSingleKeyEvenMansour_toReal_le`). The lazy-sampled bidirectional - random-permutation coupling step connecting this bad-key intersection bound to full two-sided - `Game.advantage (evenMansourRealGame program) (evenMansourIdealGame program)` remains open. + `IsCallBounded.badSingleKeyEvenMansour_toReal_le`). The final key-shifted coupling step + connecting `evenMansourRealGame` to `idealLazyHandler` via this bad-key intersection bound to + bound `Game.advantage (evenMansourRealGame program) (evenMansourIdealGame program)` remains + open. ## Main definitions @@ -73,10 +78,11 @@ We formalize four aspects of the Even–Mansour construction: `singleKeyEvenMansourEquiv`: Even–Mansour encryption, decryption, and bundled permutations. * `Cslib.Crypto.EvenMansour.preWhitenEquiv`, `postWhitenEquiv`, `preWhitenKeyRecoveryAttack`, `postWhitenKeyRecoveryAttack`: single-whitening variants and 2-query key-recovery attacks. -* `Cslib.Crypto.EvenMansour.PermQuery`, `PermOracleSpec`, `EvenMansourSpec`, `IsCallBounded`: +* `Cslib.Crypto.EvenMansour.EvenMansourSpec`, `IsCallBounded`: bidirectional cipher and primitive permutation oracle interface and separate query budgets. * `Cslib.Crypto.EvenMansour.evenMansourRealGame`, `singleKeyEvenMansourRealGame`, - `evenMansourIdealGame`: real and ideal bidirectional permutation games. + `evenMansourIdealGame`, `idealLazyHandler`: real and ideal bidirectional permutation games and the + lazy two-permutation handler. * `Cslib.Crypto.EvenMansour.isBadKeyPair`, `isBadEvenMansourKey`, `isBadSingleKeyEvenMansour`, `transcriptCipher`, `transcriptPerm`: bad-key collision predicates and transcript projections. @@ -87,9 +93,11 @@ We formalize four aspects of the Even–Mansour construction: * `Cslib.Crypto.EvenMansour.advantage_preWhitenKeyRecoveryGame_eq`, `Cslib.Crypto.EvenMansour.advantage_postWhitenKeyRecoveryGame_eq`: 2-query attacks achieve key-recovery game advantage `1 - |G|⁻¹` when either whitening key is omitted. -* `Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftLeft_eq_zero`, - `Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftRight_eq_zero`: zero advantage when - queries are restricted to one oracle. +* `Cslib.Crypto.EvenMansour.evenMansourIdealGame_eq_lazy`, + `Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftLeft_eq_zero`, + `Cslib.Crypto.EvenMansour.advantage_evenMansourRealGame_liftRight_eq_zero`: lazy two-permutation + equivalence for `evenMansourIdealGame` and zero advantage when queries are restricted to one + oracle. * `Cslib.Crypto.EvenMansour.toOuterMeasure_isBadEvenMansourKey_toReal_le`, `Cslib.Crypto.EvenMansour.toOuterMeasure_isBadSingleKeyEvenMansour_toReal_le`, `Cslib.Crypto.EvenMansour.IsCallBounded.badEvenMansourKey_toReal_le`, @@ -110,7 +118,7 @@ We formalize four aspects of the Even–Mansour construction: namespace Cslib.Crypto.EvenMansour -open Probability OracleComp +open Probability OracleComp RandomPermutation open scoped ENNReal NNReal BigOperators /-! ### Algebraic Even–Mansour cipher over an additive group -/ @@ -289,30 +297,6 @@ end Algebraic /-! ### Bidirectional ideal-permutation oracle interface and games -/ -/-- A bidirectional query to a permutation on `G`: either evaluate in the forward direction or -evaluate the inverse permutation. -/ -inductive PermQuery (G : Type) where - /-- Forward query `x ↦ P(x)`. -/ - | forward (x : G) - /-- Inverse query `y ↦ P⁻¹(y)`. -/ - | inverse (y : G) - deriving DecidableEq - -/-- The oracle specification of a bidirectional permutation on `G`. -/ -abbrev PermOracleSpec (G : Type) : OracleSpec (PermQuery G) := - fun _ => G - -/-- Answer a bidirectional permutation query using `P : Equiv.Perm G`. -/ -def evalPerm {G : Type} (P : Equiv.Perm G) : PermQuery G → G - | .forward x => P x - | .inverse y => P.symm y - -@[simp] theorem evalPerm_forward {G : Type} (P : Equiv.Perm G) (x : G) : - evalPerm P (.forward x) = P x := rfl - -@[simp] theorem evalPerm_inverse {G : Type} (P : Equiv.Perm G) (y : G) : - evalPerm P (.inverse y) = P.symm y := rfl - /-- The combined oracle interface in the Even–Mansour security experiment ([BonehShoup2023], Section 4.7): left queries (`.inl`) call the cipher permutation `E` and right queries (`.inr`) call the public primitive permutation `π`. -/ @@ -510,6 +494,100 @@ noncomputable def evenMansourIdealGame (program : OracleComp (EvenMansourSpec G) let π ← PMF.uniformOfFintype (Equiv.Perm G) return evalTwoPerms E π program +/-- Lazy bidirectional two-permutation handler for `evenMansourIdealGame`: left (cipher) queries +are answered lazily from `cache_e` and right (primitive permutation) queries are answered lazily +from `cache_π` via `RandomPermutation.answer`. -/ +noncomputable def idealLazyHandler (q : PermQuery G ⊕ PermQuery G) : + StateT (RandomPermutation.Cache G × RandomPermutation.Cache G) PMF (EvenMansourSpec G q) := + fun (cache_e, cache_π) => + match q with + | .inl qe => + (RandomPermutation.answer qe cache_e).map fun (y, cache_e') => (y, (cache_e', cache_π)) + | .inr qπ => + (RandomPermutation.answer qπ cache_π).map fun (v, cache_π') => (v, (cache_e, cache_π')) + +omit [AddGroup G] [Fintype G] [DecidableEq G] [Nonempty G] in +private theorem pure_evalTwoPerms {α : Type} (E π : Equiv.Perm G) + (program : OracleComp (EvenMansourSpec G) α) : + (PMF.pure (evalTwoPerms E π program) : PMF α) = + OracleComp.interpret + (sumHandler (fun q => PMF.pure (evalPerm E q)) (fun q => PMF.pure (evalPerm π q))) + program := by + induction program with + | pure a => rfl + | liftBind q cont ih => + change PMF.pure (evalTwoPerms E π (OracleComp.query q >>= cont)) = + OracleComp.interpret + (sumHandler (fun q => PMF.pure (evalPerm E q)) (fun q => PMF.pure (evalPerm π q))) + (OracleComp.query q >>= cont) + cases q <;> + · simp only [evalTwoPerms, sumHandler, OracleComp.interpret_bind, OracleComp.interpret_query, + Id.run_bind, PMF.monad_bind_eq_bind, PMF.pure_bind] + exact ih _ + +omit [AddGroup G] in +/-- **Ideal Even–Mansour game equals lazy bidirectional two-permutation sampling**: sampling two +independent uniform permutations `E, π ← PMF.uniformOfFintype (Equiv.Perm G)` has the exact same +output distribution as running `idealLazyHandler` from `([], [])`. -/ +theorem evenMansourIdealGame_eq_lazy (program : OracleComp (EvenMansourSpec G) Bool) : + evenMansourIdealGame program = + (((OracleComp.interpret idealLazyHandler program).run ([], [])).map Prod.fst) := by + let sim (st : RandomPermutation.Cache G × RandomPermutation.Cache G) : + PMF (Equiv.Perm G × Equiv.Perm G) := + (RandomPermutation.complete st.1).bind fun E => (RandomPermutation.complete st.2).map (E, ·) + let inv (st : RandomPermutation.Cache G × RandomPermutation.Cache G) : Prop := + RandomPermutation.IsPartialBijection st.1 ∧ RandomPermutation.IsPartialBijection st.2 + let readH (q : PermQuery G ⊕ PermQuery G) (p : Equiv.Perm G × Equiv.Perm G) : + PMF (EvenMansourSpec G q) := + sumHandler (fun q => PMF.pure (evalPerm p.1 q)) (fun q => PMF.pure (evalPerm p.2 q)) q + have hpres : ∀ q st, inv st → + ∀ a st', (a, st') ∈ (idealLazyHandler q st).support → inv st' := by + rintro (qe | qπ) ⟨c_e, c_π⟩ ⟨he, hπ⟩ a ⟨c_e', c_π'⟩ hmem + · simp only [idealLazyHandler, PMF.mem_support_map_iff] at hmem + obtain ⟨⟨a₀, ce₀⟩, hmem₀, hpair⟩ := hmem + cases hpair + exact ⟨RandomPermutation.answer_preserve_isPartialBijection qe c_e he a₀ ce₀ hmem₀, hπ⟩ + · simp only [idealLazyHandler, PMF.mem_support_map_iff] at hmem + obtain ⟨⟨a₀, cπ₀⟩, hmem₀, hpair⟩ := hmem + cases hpair + exact ⟨he, RandomPermutation.answer_preserve_isPartialBijection qπ c_π hπ a₀ cπ₀ hmem₀⟩ + have hstep : ∀ q st, inv st → + (do let (a, st') ← idealLazyHandler q st; (a, ·) <$> sim st') = + (do let p ← sim st; let y ← (·, p) <$> readH q p; pure y) := by + rintro (qe | qπ) ⟨c_e, c_π⟩ ⟨he, hπ⟩ + · have h1 := congrArg + (fun m : PMF (G × Equiv.Perm G) => + m.bind fun (y, E) => (RandomPermutation.complete c_π).map fun π => (y, (E, π))) + (RandomPermutation.answer_complete qe c_e he) + simpa only [idealLazyHandler, sim, readH, sumHandler, PMF.monad_bind_eq_bind, + PMF.monad_map_eq_map, PMF.monad_pure_eq_pure, PMF.bind_map, PMF.map_bind, + PMF.bind_bind, PMF.pure_map, PMF.pure_bind, PMF.map_comp, PMF.map, + Function.comp_def] using h1 + · have h2 := congrArg + (fun m : PMF (G × Equiv.Perm G) => + (RandomPermutation.complete c_e).bind fun E => + m.map fun (v, π) => (v, (E, π))) + (RandomPermutation.answer_complete qπ c_π hπ) + simp only [idealLazyHandler, sim, readH, sumHandler, PMF.monad_bind_eq_bind, + PMF.monad_map_eq_map, PMF.bind_bind, PMF.pure_bind, PMF.map, Function.comp_def] at h2 ⊢ + rw [PMF.bind_comm] + exact h2 + have hsim := OracleComp.run_interpret_simulation_of_invariant idealLazyHandler + (fun q p => (·, p) <$> readH q p) sim inv hpres hstep program ([], []) + ⟨RandomPermutation.isPartialBijection_nil, RandomPermutation.isPartialBijection_nil⟩ + have hsim' := congrArg (PMF.map Prod.fst) hsim + simp only [sim, RandomPermutation.complete_nil, PMF.monad_map_eq_map, + PMF.map, Function.comp_def, PMF.bind_bind, + PMF.pure_bind, PMF.bind_const] at hsim' + refine Eq.trans ?_ hsim'.symm + simp only [evenMansourIdealGame, PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] + refine congrArg ((PMF.uniformOfFintype (Equiv.Perm G)).bind) (funext fun E => ?_) + refine congrArg ((PMF.uniformOfFintype (Equiv.Perm G)).bind) (funext fun π => ?_) + rw [pure_evalTwoPerms] + simpa only [readH, PMF.monad_map_eq_map, PMF.map_comp, PMF.map, Function.comp_def, + PMF.bind_bind, PMF.pure_bind, PMF.bind_pure] using + (congrArg (PMF.map Prod.fst) (OracleComp.run_interpret_readOnly readH program (E, π))).symm + /-- For any adversary `program` that queries only the cipher oracle (`liftLeft program`), the real Even–Mansour game is identically distributed to the ideal game. -/ theorem evenMansourRealGame_liftLeft_eq_ideal (program : OracleComp (PermOracleSpec G) Bool) : diff --git a/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean b/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean index 1e4b5a4df3..73157c5e94 100644 --- a/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean +++ b/Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean @@ -13,6 +13,7 @@ public import Complexity.Languages.Probabilistic.QueryCount public import Complexity.Probability.HashFamily public import Mathlib.Data.Fintype.Perm import Complexity.Languages.Probabilistic.RandomOracle +import Complexity.Languages.Probabilistic.RandomPermutation import Complexity.Languages.Probabilistic.Simulation import Complexity.Languages.Probabilistic.UntilBad import Complexity.Probability.BitString @@ -53,33 +54,41 @@ We prove the **Luby–Rackoff theorem** ([BonehShoup2023], Section 4.4.1, Theore `G × G` at most $$\frac{2 \binom{Q}{2}}{|G|} = \frac{Q (Q - 1)}{|G|}$$ (`advantage_feistel3RandomRoundsGame_randomFunctionGame_le`). -3. **Computational PRF-to-Feistel hybrid reductions (3-round and 4-round)**: replacing keyed round - functions `F kᵢ` with independent uniform random round functions adds at most the sum of the - single-round PRF advantages (`advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le`, +3. **Computational PRF-to-Feistel hybrid reductions (3-round and 4-round) and PRP switching**: + replacing keyed round functions `F kᵢ` with independent uniform random round functions adds at + most the sum of the single-round PRF advantages + (`advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le`, `advantage_feistel3KeyedGame_randomFunctionGame_le`, and the four-round bidirectional chosen-ciphertext hybrid bound - `advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le`). + `advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le`). Combining with the + PRP/PRF switching bound on `G × G` (`advantage_idealPermGame_randomFunctionGame_le`) yields the + pseudorandom-permutation bounds against `idealPermGame` + (`advantage_feistel3HashIdealGame_idealPermGame_le`, + `advantage_feistel3RandomRoundsGame_idealPermGame_le`, + `advantage_feistel3KeyedGame_idealPermGame_le`). 4. **Three-round chosen-ciphertext separation ([BonehShoup2023], Section 4.4.2)**: with two forward encryption queries and one inverse decryption query, the explicit distinguisher `feistel3CCAAttack` accepts any three-round Feistel network with probability `1` (`eval_feistel3_feistel3CCAAttack`). When `l₀ = l₁`, the third query asks to invert the first ciphertext, so every bidirectional permutation (`feistelStrongOracle π`) and `idealStrongGame` also accept with probability `1` (`eval_feistelStrongOracle_feistel3CCAAttack_self`, - `idealStrongGame_feistel3CCAAttack_self`, `advantage_feistel3CCAAttack_self`). When `G` has - three distinct elements `l₀, l₁, l₂` (`|G| ≥ 3`), the transposition - `Equiv.swap (l₀, (l₁ - l₀) + r₀) (l₂, r₀)` is rejected - (`eval_feistelStrongOracle_swap_feistel3CCAAttack_eq_false`), - so `feistel3CCAAttack l₀ l₁ r₀` achieves strictly positive advantage at least - `(|Equiv.Perm (G × G)|)⁻¹ = ((|G|^2)!)⁻¹` against the true bidirectional random-permutation - game `idealStrongGame` (`le_advantage_feistel3CCAAttack_idealStrongGame`, - `advantage_feistel3CCAAttack_idealStrongGame_pos`). This single-transposition bound establishes - a finite positive gap for `|G| ≥ 3`, but does not establish a nonnegligible cryptographic CCA - break as the block size grows; a quantitative nonnegligible lower bound against - `idealStrongGame` (and the 4-round information-theoretic bidirectional random-round collision - bound) remains open in #748. Separately, against the independent-table bidirectional benchmark - `independentTableStrongGame`, `feistel3CCAAttack l₀ l₁ r₀` accepts with probability `|G|⁻¹` and - has exact advantage `1 - |G|⁻¹` (`eval_independentTableStrongGame_feistel3CCAAttack`, - `advantage_feistel3CCAAttack_independentTable`). + `idealStrongGame_feistel3CCAAttack_self`, `advantage_feistel3CCAAttack_self`). Whenever + `l₀ ≠ l₁`, coupling `idealStrongGame` with the forgetful bidirectional lazy sampler shows that + `idealStrongGame` accepts `feistel3CCAAttack l₀ l₁ r₀` with probability at most + `|G|⁻¹ + 4 * |G × G|⁻¹` (`idealStrongGame_feistel3CCAAttack_true_le`), giving the quantitative + nonnegligible chosen-ciphertext advantage lower bound + `1 - |G|⁻¹ - 4 * |G|⁻¹ ^ 2` against `idealStrongGame` + (`le_advantage_feistel3CCAAttack_idealStrongGame_of_ne`). In addition, when `G` has three + distinct elements `l₀, l₁, l₂` (`|G| ≥ 3`), the transposition + `Equiv.swap (l₀, (l₁ - l₀) + r₀) (l₂, r₀)` is rejected deterministically + (`eval_feistelStrongOracle_swap_feistel3CCAAttack_eq_false`, + `le_advantage_feistel3CCAAttack_idealStrongGame`, + `advantage_feistel3CCAAttack_idealStrongGame_pos`), and against the independent-table + bidirectional benchmark `independentTableStrongGame`, `feistel3CCAAttack l₀ l₁ r₀` accepts with + probability `|G|⁻¹` and has exact advantage `1 - |G|⁻¹` + (`eval_independentTableStrongGame_feistel3CCAAttack`, + `advantage_feistel3CCAAttack_independentTable`). The 4-round information-theoretic bidirectional + random-round collision bound remains open in #748. ## Main definitions @@ -88,8 +97,8 @@ We prove the **Luby–Rackoff theorem** ([BonehShoup2023], Section 4.4.1, Theore * `Cslib.Crypto.LubyRackoff.feistelNetwork`, `feistel3`, `feistel4`: multi-round, 3-round, and 4-round Feistel permutations. * `Cslib.Crypto.LubyRackoff.feistel3FixedGame`, `feistel3HashIdealGame`, - `feistel3RandomRoundsGame`, `feistel3KeyedGame`, `randomFunctionGame`: 3-round Feistel and ideal - random-function games. + `feistel3RandomRoundsGame`, `feistel3KeyedGame`, `randomFunctionGame`, `idealPermGame`: 3-round + Feistel, ideal random-function, and ideal random-permutation games. * `Cslib.Crypto.LubyRackoff.feistelStrongOracle`, `idealStrongGame`, `independentTableStrongGame`, `feistel4StrongKeyedGame`, `feistel4StrongRandomRoundsGame`, `feistel3CCAAttack`: bidirectional (forward + inverse) oracle games and the 3-query CCA attack on @@ -101,16 +110,21 @@ We prove the **Luby–Rackoff theorem** ([BonehShoup2023], Section 4.4.1, Theore conjugation identity for Feistel decryption over groups of exponent two. * `Cslib.Crypto.LubyRackoff.isDeltaUniversalHash_uniformOfFintype`: a uniform random function into `G` is `|G|⁻¹`-Δ-universal. -* `Cslib.Crypto.LubyRackoff.advantage_feistel3HashIdealGame_randomFunctionGame_le`: 3-round - Luby–Rackoff bound with Δ-universal Round 1 (`Q.choose 2 * ε + Q.choose 2 / |G|`). -* `Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_randomFunctionGame_le`: 3-round - Luby–Rackoff bound with three uniform random round functions (`2 * Q.choose 2 / |G|`). -* `Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_randomFunctionGame_le`: Boneh–Shoup - Theorem 4.6 combining the 3-round PRF hybrid reduction with the information-theoretic bound. +* `Cslib.Crypto.LubyRackoff.advantage_feistel3HashIdealGame_randomFunctionGame_le`, + `Cslib.Crypto.LubyRackoff.advantage_feistel3HashIdealGame_idealPermGame_le`: 3-round + Luby–Rackoff bounds with Δ-universal Round 1 against `randomFunctionGame` and `idealPermGame`. +* `Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_randomFunctionGame_le`, + `Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_idealPermGame_le`: 3-round + Luby–Rackoff bounds with three uniform random round functions. +* `Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_randomFunctionGame_le`, + `Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_idealPermGame_le`: Boneh–Shoup Theorem 4.6 + combining the 3-round PRF hybrid reduction with the information-theoretic PRF and PRP bounds. * `Cslib.Crypto.LubyRackoff.advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le`: 4-round bidirectional PRF-to-random-rounds hybrid bound. * `Cslib.Crypto.LubyRackoff.eval_feistel3_feistel3CCAAttack`, `Cslib.Crypto.LubyRackoff.advantage_feistel3CCAAttack_self`, + `Cslib.Crypto.LubyRackoff.idealStrongGame_feistel3CCAAttack_true_le`, + `Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame_of_ne`, `Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame`, `Cslib.Crypto.LubyRackoff.advantage_feistel3CCAAttack_independentTable`: the 3-query CCA distinguisher against 3-round Feistel. @@ -334,6 +348,13 @@ noncomputable def randomFunctionGame let table ← PMF.uniformOfFintype (G × G → G × G) OracleComp.interpret (fun p => PMF.pure (table p)) program +/-- The ideal random-permutation game on `G × G`: sample a uniform permutation +`π ← PMF.uniformOfFintype (Equiv.Perm (G × G))` and answer every query via `π p`. -/ +noncomputable def idealPermGame + (program : OracleComp (fun _ : G × G => G × G) Bool) : Game := do + let π ← PMF.uniformOfFintype (Equiv.Perm (G × G)) + OracleComp.interpret (fun p => PMF.pure (π p)) program + /-- Deduplicate queries of an adaptive program by caching the first answer to each query in an association list. -/ private def dedup {α : Type} (program : OracleComp (fun _ : G × G => G × G) α) : @@ -929,84 +950,30 @@ private theorem toOuterMeasure_hasVCollision_le {α : Type} ((OracleComp.interpret (memoize (fun _ : G × G => PMF.uniformOfFintype (G × G))) program).run qc).toOuterMeasure {x | hasVCollision x.2 = true} ≤ (n * qc.length + n.choose 2 : ℕ) * (Fintype.card G : ℝ≥0∞)⁻¹ := by - induction hn generalizing qc with - | pure a n => - change (PMF.pure (a, qc)).toOuterMeasure {x : α × List ((G × G) × (G × G)) | - hasVCollision x.2 = true} ≤ _ - simp [PMF.toOuterMeasure_pure_apply, hqc] - | liftBind p cont n _ ih => - classical - set handler := memoize (fun _ : G × G => PMF.uniformOfFintype (G × G)) - change ((handler p qc).bind fun y => - (OracleComp.interpret handler (cont y.1)).run y.2).toOuterMeasure - {x | hasVCollision x.2 = true} ≤ _ - rw [PMF.toOuterMeasure_bind_apply] - set K : ℝ≥0∞ := (n * (qc.length + 1) + n.choose 2 : ℕ) * (Fintype.card G : ℝ≥0∞)⁻¹ - have hstep_bad : - (handler p qc).toOuterMeasure {y | hasVCollision y.2 = true} ≤ - qc.length * (Fintype.card G : ℝ≥0∞)⁻¹ := by - cases hlookup : qc.lookup p with - | some r => - rw [show handler p qc = PMF.pure (r, qc) from memoize_of_some _ _ _ _ hlookup] - simp [PMF.toOuterMeasure_pure_apply, hqc] - | none => - rw [show handler p qc = (PMF.uniformOfFintype (G × G)).map (fun vw => (vw, (p, vw) :: qc)) - from memoize_of_none _ _ _ hlookup, PMF.toOuterMeasure_map_apply] - refine (le_of_eq ?_).trans (toOuterMeasure_any_vCollision_le qc) - congr 1 - ext ⟨v, w⟩ - simp [hasVCollision, hqc] - have hgrow (y : (G × G) × List ((G × G) × (G × G))) (hy : y ∈ (handler p qc).support) : - y.2.length ≤ qc.length + 1 := by - rcases y with ⟨r, qc₁⟩ - have hy' := (RandomOracle.mem_support_memoize_iff _ _ _ (r, qc₁)).mp hy - dsimp only at hy' ⊢ - rcases hy' with ⟨_, rfl⟩ | ⟨_, _, rfl⟩ - · exact Nat.le_succ _ - · rw [List.length_cons] - have hterm (y : (G × G) × List ((G × G) × (G × G))) : - (handler p qc) y * - ((OracleComp.interpret handler (cont y.1)).run y.2).toOuterMeasure - {x | hasVCollision x.2 = true} ≤ - (handler p qc) y * - ({y : (G × G) × List ((G × G) × (G × G)) | - hasVCollision y.2 = true}.indicator 1 y + K) := by - by_cases hmem : y ∈ (handler p qc).support - · refine mul_le_mul_of_nonneg_left ?_ zero_le - by_cases hbad : hasVCollision y.2 = true - · have hmem_bad : y ∈ {y : (G × G) × List ((G × G) × (G × G)) | - hasVCollision y.2 = true} := hbad - rw [Set.indicator_of_mem hmem_bad, Pi.one_apply] - exact (Probability.PMF.toOuterMeasure_le_one _ _).trans le_self_add - · have hnot_bad : y ∉ {y : (G × G) × List ((G × G) × (G × G)) | - hasVCollision y.2 = true} := hbad - rw [Set.indicator_of_notMem hnot_bad, zero_add] - have hfalse : hasVCollision y.2 = false := Bool.eq_false_iff.mpr hbad - refine (ih y.1 hfalse).trans ?_ - simp only [K] - gcongr - exact hgrow y hmem - · rw [(PMF.apply_eq_zero_iff _ _).mpr hmem, zero_mul, zero_mul] - calc ∑' y, (handler p qc) y * - ((OracleComp.interpret handler (cont y.1)).run y.2).toOuterMeasure - {x | hasVCollision x.2 = true} - ≤ ∑' y, (handler p qc) y * - ({y : (G × G) × List ((G × G) × (G × G)) | - hasVCollision y.2 = true}.indicator 1 y + K) := - ENNReal.tsum_le_tsum hterm - _ = (handler p qc).toOuterMeasure {y | hasVCollision y.2 = true} + K := by - simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, - PMF.toOuterMeasure_apply] - congr 1 - refine tsum_congr fun y => ?_ - by_cases hy : y ∈ {y : (G × G) × List ((G × G) × (G × G)) | hasVCollision y.2 = true} - · rw [Set.indicator_of_mem hy, Set.indicator_of_mem hy, Pi.one_apply, mul_one] - · rw [Set.indicator_of_notMem hy, Set.indicator_of_notMem hy, mul_zero] - _ ≤ qc.length * (Fintype.card G : ℝ≥0∞)⁻¹ + K := add_le_add hstep_bad le_rfl - _ = ((n + 1) * qc.length + (n + 1).choose 2 : ℕ) * (Fintype.card G : ℝ≥0∞)⁻¹ := by - simp only [K, Nat.choose_succ_succ' n 1, Nat.choose_one_right, Nat.cast_add, - Nat.cast_mul, Nat.cast_one] - ring + refine RandomPermutation.toOuterMeasure_bad_choose_two_le + (bad := fun s : List ((G × G) × (G × G)) => hasVCollision s = true) + List.length (Fintype.card G : ℝ≥0∞)⁻¹ + (fun p s hs => ?_) (fun p s _ y hy _ => ?_) hn (Bool.eq_false_iff.mp hqc) + · have hs' : hasVCollision s = false := Bool.eq_false_iff.mpr hs + cases hlookup : s.lookup p with + | some r => + rw [show memoize (fun _ : G × G => PMF.uniformOfFintype (G × G)) p s = PMF.pure (r, s) + from memoize_of_some _ _ _ _ hlookup] + simp [PMF.toOuterMeasure_pure_apply, hs'] + | none => + rw [show memoize (fun _ : G × G => PMF.uniformOfFintype (G × G)) p s = + (PMF.uniformOfFintype (G × G)).map (fun vw => (vw, (p, vw) :: s)) + from memoize_of_none _ _ _ hlookup, PMF.toOuterMeasure_map_apply] + refine (le_of_eq ?_).trans (toOuterMeasure_any_vCollision_le s) + congr 1 + ext ⟨v, w⟩ + simp [hasVCollision, hs'] + · rcases y with ⟨r, qc₁⟩ + have hy' := (RandomOracle.mem_support_memoize_iff _ _ _ (r, qc₁)).mp hy + dsimp only at hy' ⊢ + rcases hy' with ⟨_, rfl⟩ | ⟨_, _, rfl⟩ + · exact Nat.le_succ _ + · rw [List.length_cons] /-- Bound on the expected bad-event probability in `idealRoundHandler` averaged over `k₁ ← seed₁`. -/ @@ -1205,6 +1172,66 @@ theorem advantage_feistel3RandomRoundsGame_randomFunctionGame_le (randomFunctionGame program) : ℝ) ≤ _ at h linarith [h] +omit [AddGroup G] in +/-- **PRP/PRF switching bound on `G × G`**: for any `Q`-query adaptive adversary, `idealPermGame` +and `randomFunctionGame` have distinguishing advantage at most `Q.choose 2 / |G| ^ 2`. -/ +theorem advantage_idealPermGame_randomFunctionGame_le + {program : OracleComp (fun _ : G × G => G × G) Bool} {Q : ℕ} + (hQ : OracleComp.IsQueryBounded program Q) : + (Game.advantage (idealPermGame program) (randomFunctionGame program) : ℝ) ≤ + (Q.choose 2 : ℝ) * ((Fintype.card G : ℝ)⁻¹) ^ 2 := by + rw [Game.coe_advantage] + simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, idealPermGame, + randomFunctionGame, Probability.PMF.monad_bind_eq_bind] + have h := RandomPermutation.abs_sub_uniformPerm_uniformFunc_le hQ PMF.pure true + simp only [Probability.PMF.monad_bind_eq_bind, PMF.bind_pure] at h + refine h.trans_eq ?_ + rw [Fintype.card_prod, Nat.cast_mul, mul_inv, sq] + +/-- **3-round Luby–Rackoff PRP bound with Δ-universal Round 1**: against a uniform random +permutation on `G × G` (`idealPermGame`), the distinguishing advantage of a `Q`-query adversary is +at most `Q.choose 2 * ε.toReal + Q.choose 2 / |G| + Q.choose 2 / |G| ^ 2`. -/ +theorem advantage_feistel3HashIdealGame_idealPermGame_le + {seed₁ : PMF K₁} {h₁ : K₁ → G → G} {ε : ℝ≥0∞} (hh₁ : IsDeltaUniversalHash seed₁ h₁ ε) + (hε : ε ≠ ⊤) {program : OracleComp (fun _ : G × G => G × G) Bool} {Q : ℕ} + (hQ : OracleComp.IsQueryBounded program Q) : + (Game.advantage (feistel3HashIdealGame seed₁ h₁ program) + (idealPermGame program) : ℝ) ≤ + (Q.choose 2 : ℝ) * ε.toReal + (Q.choose 2 : ℝ) * (Fintype.card G : ℝ)⁻¹ + + (Q.choose 2 : ℝ) * ((Fintype.card G : ℝ)⁻¹) ^ 2 := by + have htri : + (Game.advantage (feistel3HashIdealGame seed₁ h₁ program) (idealPermGame program) : ℝ) ≤ + (Game.advantage (feistel3HashIdealGame seed₁ h₁ program) + (randomFunctionGame program) : ℝ) + + (Game.advantage (randomFunctionGame program) (idealPermGame program) : ℝ) := by + exact_mod_cast Game.advantage_triangle + (feistel3HashIdealGame seed₁ h₁ program) (randomFunctionGame program) (idealPermGame program) + rw [Game.advantage_comm (randomFunctionGame program) (idealPermGame program)] at htri + have h1 := advantage_feistel3HashIdealGame_randomFunctionGame_le hh₁ hε hQ + have h2 := advantage_idealPermGame_randomFunctionGame_le hQ + linarith + +/-- **Classical 3-round Luby–Rackoff PRP bound**: three Feistel rounds with independent uniform +random round functions on `G` are indistinguishable from a uniform random permutation on `G × G` +(`idealPermGame`) up to `2 * Q.choose 2 / |G| + Q.choose 2 / |G| ^ 2`. -/ +theorem advantage_feistel3RandomRoundsGame_idealPermGame_le + {program : OracleComp (fun _ : G × G => G × G) Bool} {Q : ℕ} + (hQ : OracleComp.IsQueryBounded program Q) : + (Game.advantage (feistel3RandomRoundsGame program) + (idealPermGame program) : ℝ) ≤ + 2 * (Q.choose 2 : ℝ) * (Fintype.card G : ℝ)⁻¹ + + (Q.choose 2 : ℝ) * ((Fintype.card G : ℝ)⁻¹) ^ 2 := by + have htri : + (Game.advantage (feistel3RandomRoundsGame program) (idealPermGame program) : ℝ) ≤ + (Game.advantage (feistel3RandomRoundsGame program) (randomFunctionGame program) : ℝ) + + (Game.advantage (randomFunctionGame program) (idealPermGame program) : ℝ) := by + exact_mod_cast Game.advantage_triangle + (feistel3RandomRoundsGame program) (randomFunctionGame program) (idealPermGame program) + rw [Game.advantage_comm (randomFunctionGame program) (idealPermGame program)] at htri + have h1 := advantage_feistel3RandomRoundsGame_randomFunctionGame_le hQ + have h2 := advantage_idealPermGame_randomFunctionGame_le hQ + linarith + end LubyRackoff3 /-! ### 3-round PRF-to-Feistel hybrid reductions (Boneh–Shoup Theorem 4.6) -/ @@ -1444,6 +1471,38 @@ theorem advantage_feistel3KeyedGame_randomFunctionGame_le exact_mod_cast htri linarith +/-- **The Luby–Rackoff PRP theorem** ([BonehShoup2023], Theorem 4.6; [LubyRackoff1988]): a 3-round +Feistel cipher built from three independently keyed instances of a round function `F` has +distinguishing advantage against a uniform random permutation on `G × G` (`idealPermGame`) at most +`ε₁ + ε₂ + ε₃ + 2 * Q.choose 2 / |G| + Q.choose 2 / |G| ^ 2`. -/ +theorem advantage_feistel3KeyedGame_idealPermGame_le + {keyGen : PMF K} {F : K → G → G} + {program : OracleComp (fun _ : G × G => G × G) Bool} {Q : ℕ} + (hQ : OracleComp.IsQueryBounded program Q) {ε₁ ε₂ ε₃ : ℝ} + (h₁ : ∀ f₂ f₃, + (Game.advantage (prfSingleRealGame keyGen F (feistel3Reduction₁ f₂ f₃ program)) + (prfSingleIdealGame (feistel3Reduction₁ f₂ f₃ program)) : ℝ) ≤ ε₁) + (h₂ : ∀ f₁ f₃, + (Game.advantage (prfSingleRealGame keyGen F (feistel3Reduction₂ f₁ f₃ program)) + (prfSingleIdealGame (feistel3Reduction₂ f₁ f₃ program)) : ℝ) ≤ ε₂) + (h₃ : ∀ f₁ f₂, + (Game.advantage (prfSingleRealGame keyGen F (feistel3Reduction₃ f₁ f₂ program)) + (prfSingleIdealGame (feistel3Reduction₃ f₁ f₂ program)) : ℝ) ≤ ε₃) : + (Game.advantage (feistel3KeyedGame keyGen F program) + (idealPermGame program) : ℝ) ≤ + ε₁ + ε₂ + ε₃ + 2 * (Q.choose 2 : ℝ) * (Fintype.card G : ℝ)⁻¹ + + (Q.choose 2 : ℝ) * ((Fintype.card G : ℝ)⁻¹) ^ 2 := by + have htri : + (Game.advantage (feistel3KeyedGame keyGen F program) (idealPermGame program) : ℝ) ≤ + (Game.advantage (feistel3KeyedGame keyGen F program) + (feistel3RandomRoundsGame program) : ℝ) + + (Game.advantage (feistel3RandomRoundsGame program) (idealPermGame program) : ℝ) := by + exact_mod_cast Game.advantage_triangle (feistel3KeyedGame keyGen F program) + (feistel3RandomRoundsGame program) (idealPermGame program) + have hprf := advantage_feistel3KeyedGame_feistel3RandomRoundsGame_le h₁ h₂ h₃ + have hlr := advantage_feistel3RandomRoundsGame_idealPermGame_le hQ + linarith + /-- Concrete instantiation of the 3-round Luby–Rackoff theorem on `BitString n` (block size `2n`): the information-theoretic collision error is at most `2 * Q.choose 2 / 2 ^ n`. -/ theorem advantage_feistel3RandomRoundsGame_bitString_le (n : ℕ) @@ -1733,6 +1792,185 @@ theorem advantage_feistel3CCAAttack_independentTable (f₁ f₂ f₃ : G → G) inv_le_one_of_one_le₀ (by exact_mod_cast Fintype.card_pos) exact abs_of_nonneg (sub_nonneg.mpr hle) +private theorem uniformOfFintype_prod_map_decide_add_snd_true (a t : G) : + ((PMF.uniformOfFintype (G × G)).map (fun lr : G × G => decide (a + lr.2 = t))) true = + (Fintype.card G : ℝ≥0∞)⁻¹ := by + have hsnd : + (PMF.uniformOfFintype (G × G)).map Prod.snd = PMF.uniformOfFintype G := by + rw [← Probability.PMF.uniformOfFintype_map_equiv (Equiv.prodComm G G), PMF.map_comp] + exact Probability.PMF.uniformOfFintype_prod_map_fst + have hshift : + (PMF.uniformOfFintype G).map (Equiv.addLeft a) = PMF.uniformOfFintype G := + Probability.PMF.uniformOfFintype_map_equiv (Equiv.addLeft a) + have hmap : + (PMF.uniformOfFintype (G × G)).map (fun lr : G × G => decide (a + lr.2 = t)) = + (PMF.uniformOfFintype G).map (fun y => decide (y = t)) := by + calc (PMF.uniformOfFintype (G × G)).map (fun lr : G × G => decide (a + lr.2 = t)) + = (((PMF.uniformOfFintype (G × G)).map Prod.snd).map (Equiv.addLeft a)).map + (fun y => decide (y = t)) := by + simp [PMF.map_comp, Function.comp_def] + _ = (PMF.uniformOfFintype G).map (fun y => decide (y = t)) := by + rw [hsnd, hshift] + rw [hmap, ← PMF.toOuterMeasure_apply_singleton, PMF.toOuterMeasure_map_apply] + have hpre : (fun y : G => decide (y = t)) ⁻¹' {true} = {t} := by + ext y + simp + rw [hpre, PMF.toOuterMeasure_apply_singleton, PMF.uniformOfFintype_apply] + +/-- When `l₀ ≠ l₁`, the true bidirectional random-permutation game `idealStrongGame` accepts +`feistel3CCAAttack l₀ l₁ r₀` with probability at most `|G|⁻¹ + 4 * |G × G|⁻¹`. -/ +theorem idealStrongGame_feistel3CCAAttack_true_le {l₀ l₁ : G} (r₀ : G) (h01 : l₀ ≠ l₁) : + idealStrongGame (feistel3CCAAttack l₀ l₁ r₀) true ≤ + (Fintype.card G : ℝ≥0∞)⁻¹ + 4 * (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by + have hint (π : Equiv.Perm (G × G)) : + OracleComp.interpret (feistelStrongOracle π) (feistel3CCAAttack l₀ l₁ r₀) = + OracleComp.interpret (fun q => PMF.pure (RandomPermutation.evalPerm π q)) + (RandomPermutation.liftBoolProd (feistel3CCAAttack l₀ l₁ r₀)) := by + rw [RandomPermutation.liftBoolProd, OracleComp.interpret_interpret] + congr 1 + funext ⟨b, p⟩ + cases b <;> simp [feistelStrongOracle] + have hgame : + idealStrongGame (feistel3CCAAttack l₀ l₁ r₀) = + (PMF.uniformOfFintype (Equiv.Perm (G × G))).bind fun π => + OracleComp.interpret (fun q => PMF.pure (RandomPermutation.evalPerm π q)) + (RandomPermutation.liftBoolProd (feistel3CCAAttack l₀ l₁ r₀)) := by + simp only [idealStrongGame, Probability.PMF.monad_bind_eq_bind, hint] + have hswitch := RandomPermutation.uniformPerm_bind_apply_le_forgetful + (RandomPermutation.isQueryBounded_liftBoolProd (isQueryBounded_feistel3CCAAttack l₀ l₁ r₀)) + PMF.pure true + simp only [Probability.PMF.monad_bind_eq_bind, PMF.bind_pure] at hswitch + rw [← hgame] at hswitch + have hp10 : (l₁, r₀) ≠ (l₀, r₀) := fun h => h01 (congrArg Prod.fst h).symm + have hforget : + (((OracleComp.interpret RandomPermutation.forgetfulAnswer + (RandomPermutation.liftBoolProd (feistel3CCAAttack l₀ l₁ r₀))).run []).map + Prod.fst) true ≤ + (Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by + have hrun : + (((OracleComp.interpret RandomPermutation.forgetfulAnswer + (RandomPermutation.liftBoolProd (feistel3CCAAttack l₀ l₁ r₀))).run []).map Prod.fst) = + (PMF.uniformOfFintype (G × G)).bind fun vw₀ => + (PMF.uniformOfFintype (G × G)).bind fun vw₁ => + (RandomPermutation.forgetfulAnswer + (.inverse (vw₀.1, (l₁ - l₀) + vw₀.2)) + [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)]).map + (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀)) := by + simp only [feistel3CCAAttack, RandomPermutation.liftBoolProd, + RandomPermutation.PermQuery.ofBoolProd, + OracleComp.interpret_bind, OracleComp.interpret_query, OracleComp.interpret_pure, + StateT.run_bind, StateT.run_pure] + dsimp only [StateT.run, RandomPermutation.forgetfulAnswer] + simp only [List.lookup, beq_eq_false_iff_ne.mpr hp10, + Probability.PMF.monad_bind_eq_bind, Probability.PMF.monad_pure_eq_pure, + PMF.bind_map, PMF.map_bind, PMF.pure_map, Function.comp_def] + rfl + rw [hrun, PMF.bind_apply] + have hvw₀ (vw₀ : G × G) : + ((PMF.uniformOfFintype (G × G)).bind fun vw₁ => + (RandomPermutation.forgetfulAnswer + (.inverse (vw₀.1, (l₁ - l₀) + vw₀.2)) + [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)]).map + (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true ≤ + (Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by + set q₃ : G × G := (vw₀.1, (l₁ - l₀) + vw₀.2) + have hvw₀_ne : vw₀ ≠ q₃ := fun h => by + have h2 := congrArg Prod.snd h + dsimp only [q₃] at h2 + exact h01 (sub_eq_zero.mp (add_right_cancel ((zero_add vw₀.2).trans h2)).symm).symm + rw [PMF.bind_apply] + have hvw₁ (vw₁ : G × G) : + (PMF.uniformOfFintype (G × G)) vw₁ * + ((RandomPermutation.forgetfulAnswer (.inverse q₃) + [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)]).map + (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true ≤ + (PMF.uniformOfFintype (G × G)) vw₁ * (Fintype.card G : ℝ≥0∞)⁻¹ + + ({q₃} : Set (G × G)).indicator (PMF.uniformOfFintype (G × G)) vw₁ := by + by_cases h13 : vw₁ = q₃ + · rw [Set.indicator_of_mem (Set.mem_singleton_iff.mpr h13)] + calc (PMF.uniformOfFintype (G × G)) vw₁ * + ((RandomPermutation.forgetfulAnswer (.inverse q₃) + [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)]).map + (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true + ≤ (PMF.uniformOfFintype (G × G)) vw₁ * 1 := + mul_le_mul_of_nonneg_left (PMF.coe_le_one _ true) zero_le + _ = (PMF.uniformOfFintype (G × G)) vw₁ := mul_one _ + _ ≤ (PMF.uniformOfFintype (G × G)) vw₁ * (Fintype.card G : ℝ≥0∞)⁻¹ + + (PMF.uniformOfFintype (G × G)) vw₁ := le_add_self + · rw [Set.indicator_of_notMem (fun h => h13 (Set.mem_singleton_iff.mp h)), add_zero] + have hinv : + RandomPermutation.invLookup [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)] q₃ = none := by + simp [RandomPermutation.invLookup, Ne.symm h13, Ne.symm hvw₀_ne] + have hnone : + ((RandomPermutation.forgetfulAnswer (.inverse q₃) + [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)]).map + (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true = + (Fintype.card G : ℝ≥0∞)⁻¹ := by + dsimp only [RandomPermutation.forgetfulAnswer] + rw [hinv, PMF.map_comp] + exact uniformOfFintype_prod_map_decide_add_snd_true (-vw₀.1) (-vw₁.1 + r₀) + rw [hnone] + calc ∑' vw₁, (PMF.uniformOfFintype (G × G)) vw₁ * + ((RandomPermutation.forgetfulAnswer (.inverse q₃) + [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)]).map + (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true + ≤ ∑' vw₁, ((PMF.uniformOfFintype (G × G)) vw₁ * (Fintype.card G : ℝ≥0∞)⁻¹ + + ({q₃} : Set (G × G)).indicator (PMF.uniformOfFintype (G × G)) vw₁) := + ENNReal.tsum_le_tsum hvw₁ + _ = (Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by + rw [ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + ← PMF.toOuterMeasure_apply, PMF.toOuterMeasure_apply_singleton, + PMF.uniformOfFintype_apply] + calc ∑' vw₀, (PMF.uniformOfFintype (G × G)) vw₀ * + ((PMF.uniformOfFintype (G × G)).bind fun vw₁ => + (RandomPermutation.forgetfulAnswer + (.inverse (vw₀.1, (l₁ - l₀) + vw₀.2)) + [((l₁, r₀), vw₁), ((l₀, r₀), vw₀)]).map + (fun x => decide (-vw₀.1 + x.1.2 = -vw₁.1 + r₀))) true + ≤ ∑' vw₀, (PMF.uniformOfFintype (G × G)) vw₀ * + ((Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹) := + ENNReal.tsum_le_tsum fun vw₀ => mul_le_mul_of_nonneg_left (hvw₀ vw₀) zero_le + _ = (Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by + rw [ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul] + have hchoose : ((Nat.choose 3 2 : ℕ) : ℝ≥0∞) = 3 := rfl + rw [hchoose] at hswitch + calc idealStrongGame (feistel3CCAAttack l₀ l₁ r₀) true + ≤ ((Fintype.card G : ℝ≥0∞)⁻¹ + (Fintype.card (G × G) : ℝ≥0∞)⁻¹) + + 3 * (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := + hswitch.trans (add_le_add hforget le_rfl) + _ = (Fintype.card G : ℝ≥0∞)⁻¹ + 4 * (Fintype.card (G × G) : ℝ≥0∞)⁻¹ := by + ring + +/-- **Quantitative nonnegligible CCA advantage lower bound against `idealStrongGame`** +([BonehShoup2023], Section 4.4.2): whenever `l₀ ≠ l₁`, the 3-query chosen-ciphertext distinguisher +`feistel3CCAAttack l₀ l₁ r₀` distinguishes any 3-round Feistel network `feistel3 f₁ f₂ f₃` from a +uniform random permutation on `G × G` (`idealStrongGame`) with advantage at least +`1 - |G|⁻¹ - 4 * |G|⁻¹ ^ 2`. -/ +theorem le_advantage_feistel3CCAAttack_idealStrongGame_of_ne (f₁ f₂ f₃ : G → G) {l₀ l₁ r₀ : G} + (h01 : l₀ ≠ l₁) : + 1 - (Fintype.card G : ℝ)⁻¹ - 4 * ((Fintype.card G : ℝ)⁻¹) ^ 2 ≤ + (Game.advantage + (OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) + (feistel3CCAAttack l₀ l₁ r₀)) + (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀)) : ℝ) := by + have hcardG : (Fintype.card G : ℝ≥0∞) ≠ 0 := by exact_mod_cast Fintype.card_ne_zero + have hcardGG : (Fintype.card (G × G) : ℝ≥0∞) ≠ 0 := by exact_mod_cast Fintype.card_ne_zero + have h1_top : (Fintype.card G : ℝ≥0∞)⁻¹ ≠ ⊤ := ENNReal.inv_ne_top.mpr hcardG + have h2_top : 4 * (Fintype.card (G × G) : ℝ≥0∞)⁻¹ ≠ ⊤ := + ENNReal.mul_ne_top ENNReal.ofNat_ne_top (ENNReal.inv_ne_top.mpr hcardGG) + have htrue := ENNReal.toReal_mono (ENNReal.add_ne_top.mpr ⟨h1_top, h2_top⟩) + (idealStrongGame_feistel3CCAAttack_true_le r₀ h01) + rw [ENNReal.toReal_add h1_top h2_top, ENNReal.toReal_mul, ENNReal.toReal_ofNat, + ENNReal.toReal_inv, ENNReal.toReal_inv, ENNReal.toReal_natCast, ENNReal.toReal_natCast, + Fintype.card_prod, Nat.cast_mul, mul_inv, ← sq] at htrue + rw [Game.coe_advantage, eval_feistel3_feistel3CCAAttack] + simp only [Game.succProbability, ENNReal.coe_toNNReal_eq_toReal, PMF.pure_apply_self, + ENNReal.toReal_one] + have hle_abs : + 1 - (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀) true).toReal ≤ + |1 - (idealStrongGame (feistel3CCAAttack l₀ l₁ r₀) true).toReal| := le_abs_self _ + linarith + /-- 4-round Feistel strong (bidirectional) game with four independent keyed round functions `F k₁, F k₂, F k₃, F k₄`. -/ noncomputable def feistel4StrongKeyedGame (keyGen : PMF K) (F : K → G → G) diff --git a/Complexity/Languages/Probabilistic/RandomPermutation.lean b/Complexity/Languages/Probabilistic/RandomPermutation.lean new file mode 100644 index 0000000000..bd9cd86d22 --- /dev/null +++ b/Complexity/Languages/Probabilistic/RandomPermutation.lean @@ -0,0 +1,1327 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Languages.Probabilistic.RandomOracle +public import Complexity.Languages.Probabilistic.UntilBad +public import Mathlib.Data.Fintype.Perm +import Complexity.Probability.PMF.Event +import Complexity.Probability.PMF.Uniform +import Mathlib.Data.Finset.Card +import Mathlib.Data.Nat.Choose.Basic +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Ring + +/-! +# Lazy sampling of random permutations and the PRP/PRF switching lemma + +A bidirectional permutation oracle (`PermOracleSpec α`) answers forward queries (`.forward x`) and +inverse queries (`.inverse y`) on a finite type `α`. We provide two lazy stateful samplers over an +association-list cache `Cache α = List (α × α)`: + +1. **Exact without-replacement lazy permutation (`RandomPermutation.answer`)**: on a cache hit, + return the recorded image or preimage; on a cache miss, sample uniformly from the remaining + unused range elements (`unusedRange cache`) for a forward query or from the remaining unused + domain elements (`unusedDomain cache`) for an inverse query. Using + `OracleComp.run_interpret_simulation_of_invariant` and uniform completion `complete` over the + set `extPerms cache` of permutations extending the partial bijection, we prove that adaptive + execution against `answer` followed by `complete` has the exact same joint distribution as + sampling `π ← PMF.uniformOfFintype (Equiv.Perm α)` eagerly (`run_interpret_answer_complete`, + `uniform_interpret_eq_lazy`). +2. **Forgetful with-replacement lazy permutation (`RandomPermutation.forgetfulAnswer`, + [BonehShoup2023], Section 4.7)**: on a cache miss, sample uniformly from all of `α` without + domain or range exclusion. By coupling `answer` and `forgetfulAnswer` via resampling and + `OracleComp.IdenticalUntilBad`, any `Q`-query adaptive distinguisher has distinguishing + advantage at most `Q.choose 2 / |α|` between a uniformly random permutation + `π ← PMF.uniformOfFintype (Equiv.Perm α)` and `forgetfulAnswer` + (`abs_sub_uniformPerm_forgetful_le`). On forward-only programs (`liftForward`), + `forgetfulAnswer` coincides with `memoize (fun _ => PMF.uniformOfFintype α)` and therefore with + a uniformly random function `f ← PMF.uniformOfFintype (α → α)`, yielding the classical + **PRP/PRF switching lemma** (`abs_sub_uniformPerm_uniformFunc_le`, [BonehShoup2023], + Section 4.4, Theorem 4.4). + +## Main definitions + +* `Cslib.RandomPermutation.PermQuery`, `PermOracleSpec`, `evalPerm`, `liftForward`, `liftBoolProd`: + bidirectional permutation queries, oracle specification, deterministic evaluation, and query + liftings. +* `Cslib.RandomPermutation.Cache`, `invLookup`, `AgreesWith`, `IsPartialBijection`, `extPerms`, + `unusedDomain`, `unusedRange`: partial bijection caches and extension sets. +* `Cslib.RandomPermutation.answer`, `complete`, `forgetfulAnswer`: exact and forgetful lazy + bidirectional permutation samplers and uniform completion. + +## Main results + +* `Cslib.RandomPermutation.answer_complete`, + `Cslib.RandomPermutation.run_interpret_answer_complete`, + `Cslib.RandomPermutation.uniform_interpret_eq_lazy`: exact eager/lazy equivalence for + bidirectional random permutations. +* `Cslib.RandomPermutation.toOuterMeasure_bad_choose_two_le`: quadratic union bound + `(n * size s + n.choose 2) * δ` for bad events with linearly growing step probability. +* `Cslib.RandomPermutation.uniformPerm_bind_apply_le_forgetful`, + `Cslib.RandomPermutation.abs_sub_uniformPerm_forgetful_le`: bidirectional random-permutation + switching bounds (`Q.choose 2 / |α|`). +* `Cslib.RandomPermutation.abs_sub_uniformPerm_uniformFunc_le`: the PRP/PRF switching lemma + ([BonehShoup2023], Section 4.4, Theorem 4.4). + +## References + +* [D. Boneh, V. Shoup, *A Graduate Course in Applied Cryptography*, + Version 0.6][BonehShoup2023], Sections 4.4 and 4.7 (Theorems 4.4 and 4.7). +-/ + +@[expose] public section + +namespace Cslib.RandomPermutation + +open Probability OracleComp +open scoped ENNReal NNReal BigOperators + +/-! ### Bidirectional permutation query interface -/ + +/-- A bidirectional query to a permutation on `α`: either evaluate in the forward direction or +evaluate the inverse permutation. -/ +inductive PermQuery (α : Type) where + /-- Forward query `x ↦ π(x)`. -/ + | forward (x : α) + /-- Inverse query `y ↦ π⁻¹(y)`. -/ + | inverse (y : α) + deriving DecidableEq + +/-- The oracle specification of a bidirectional permutation on `α`. -/ +abbrev PermOracleSpec (α : Type) : OracleSpec (PermQuery α) := + fun _ => α + +/-- Deterministically answer a bidirectional permutation query using `π : Equiv.Perm α`. -/ +def evalPerm {α : Type} (π : Equiv.Perm α) : PermQuery α → α + | .forward x => π x + | .inverse y => π.symm y + +@[simp] theorem evalPerm_forward {α : Type} (π : Equiv.Perm α) (x : α) : + evalPerm π (.forward x) = π x := rfl + +@[simp] theorem evalPerm_inverse {α : Type} (π : Equiv.Perm α) (y : α) : + evalPerm π (.inverse y) = π.symm y := rfl + +/-- Lift a forward-only oracle program into a bidirectional permutation oracle program. -/ +def liftForward {α β : Type} (program : OracleComp (fun _ : α => α) β) : + OracleComp (PermOracleSpec α) β := + OracleComp.interpret (fun x => OracleComp.query (spec := PermOracleSpec α) (.forward x)) program + +/-- Interpreting `liftForward program` against `evalPerm π` is interpreting `program` against +`π`. -/ +theorem interpret_evalPerm_liftForward {α β : Type} (π : Equiv.Perm α) + (program : OracleComp (fun _ : α => α) β) : + OracleComp.interpret (fun q => PMF.pure (evalPerm π q)) (liftForward program) = + OracleComp.interpret (fun x => PMF.pure (π x)) program := by + rw [liftForward, OracleComp.interpret_interpret] + simp + +/-- Lifting a forward-only program preserves query bounds. -/ +theorem isQueryBounded_liftForward {α β : Type} {program : OracleComp (fun _ : α => α) β} {Q : ℕ} + (hQ : IsQueryBounded program Q) : IsQueryBounded (liftForward program) Q := by + induction hQ with + | pure a n => exact IsCostBounded.pure a n + | liftBind x cont n _ ih => + change IsQueryBounded (OracleComp.query (spec := PermOracleSpec α) (.forward x) >>= + fun y => liftForward (cont y)) (n + 1) + simpa [Nat.add_comm] using + (IsCostBounded.query (spec := PermOracleSpec α) (.forward x)).bind ih + +/-- Convert a boolean-tagged query `(false, x)` (forward) or `(true, y)` (inverse) into a +`PermQuery α`. -/ +def PermQuery.ofBoolProd {α : Type} : Bool × α → PermQuery α + | (false, x) => .forward x + | (true, y) => .inverse y + +@[simp] theorem PermQuery.ofBoolProd_false {α : Type} (x : α) : + PermQuery.ofBoolProd (false, x) = .forward x := rfl + +@[simp] theorem PermQuery.ofBoolProd_true {α : Type} (y : α) : + PermQuery.ofBoolProd (true, y) = .inverse y := rfl + +/-- Lift a `Bool × α` bidirectional oracle program into a `PermOracleSpec α` program. -/ +def liftBoolProd {α β : Type} (program : OracleComp (fun _ : Bool × α => α) β) : + OracleComp (PermOracleSpec α) β := + OracleComp.interpret + (fun q => OracleComp.query (spec := PermOracleSpec α) (PermQuery.ofBoolProd q)) program + +/-- Lifting a `Bool × α` program preserves query bounds. -/ +theorem isQueryBounded_liftBoolProd {α β : Type} + {program : OracleComp (fun _ : Bool × α => α) β} {Q : ℕ} + (hQ : IsQueryBounded program Q) : IsQueryBounded (liftBoolProd program) Q := by + induction hQ with + | pure a n => exact IsCostBounded.pure a n + | liftBind q cont n _ ih => + change IsQueryBounded + (OracleComp.query (spec := PermOracleSpec α) (PermQuery.ofBoolProd q) >>= + fun y => liftBoolProd (cont y)) (n + 1) + simpa [Nat.add_comm] using + (IsCostBounded.query (spec := PermOracleSpec α) (PermQuery.ofBoolProd q)).bind ih + +/-! ### Partial bijection cache and lookup lemmas -/ + +/-- A partial permutation table stored as a list of input-output pairs `(x, y)`. -/ +abbrev Cache (α : Type) := List (α × α) + +variable {α : Type} [DecidableEq α] + +/-- Lookup the preimage `x` of `y` in `cache` by searching `(y, x)` in `cache.map Prod.swap`. -/ +def invLookup (cache : Cache α) (y : α) : Option α := + (cache.map Prod.swap).lookup y + +@[simp] theorem invLookup_nil (y : α) : invLookup ([] : Cache α) y = none := rfl + +theorem invLookup_cons (e : α × α) (cache : Cache α) (y : α) : + invLookup (e :: cache) y = + match y == e.2 with + | true => some e.1 + | false => invLookup cache y := rfl + +theorem mem_of_lookup_eq_some {cache : Cache α} {x y : α} (h : cache.lookup x = some y) : + (x, y) ∈ cache := by + induction cache with + | nil => cases h + | cons e rest ih => + rw [List.lookup_cons] at h + cases hxe : x == e.1 with + | true => + rw [hxe] at h + dsimp at h + obtain rfl : e.2 = y := Option.some.inj h + obtain rfl : x = e.1 := eq_of_beq hxe + exact List.mem_cons_self + | false => + rw [hxe] at h + exact List.mem_cons_of_mem e (ih h) + +theorem mem_of_invLookup_eq_some {cache : Cache α} {y x : α} (h : invLookup cache y = some x) : + (x, y) ∈ cache := by + have hswap := mem_of_lookup_eq_some h + rw [List.mem_map] at hswap + obtain ⟨⟨a, b⟩, hmem, heq⟩ := hswap + dsimp [Prod.swap] at heq + obtain ⟨rfl, rfl⟩ := Prod.mk.inj heq + exact hmem + +theorem lookup_eq_none_iff {cache : Cache α} {x : α} : + cache.lookup x = none ↔ ∀ e ∈ cache, e.1 ≠ x := by + induction cache with + | nil => simp + | cons e rest ih => + rw [List.lookup_cons, List.forall_mem_cons] + cases hxe : x == e.1 with + | true => + have hx : e.1 = x := (eq_of_beq hxe).symm + simp [hx] + | false => + have hx : e.1 ≠ x := Ne.symm (beq_eq_false_iff_ne.mp hxe) + simp [hx, ih] + +theorem invLookup_eq_none_iff {cache : Cache α} {y : α} : + invLookup cache y = none ↔ ∀ e ∈ cache, e.2 ≠ y := by + induction cache with + | nil => simp + | cons e rest ih => + rw [invLookup_cons, List.forall_mem_cons] + cases hye : y == e.2 with + | true => + have hy : e.2 = y := (eq_of_beq hye).symm + simp [hy] + | false => + have hy : e.2 ≠ y := Ne.symm (beq_eq_false_iff_ne.mp hye) + simp [hy, ih] + +/-- A permutation `π : Equiv.Perm α` agrees with `cache` if `π e.1 = e.2` for all `e ∈ cache`. -/ +def AgreesWith (cache : Cache α) (π : Equiv.Perm α) : Prop := + ∀ e ∈ cache, π e.1 = e.2 + +instance decidableAgreesWith (cache : Cache α) (π : Equiv.Perm α) : + Decidable (AgreesWith cache π) := + inferInstanceAs (Decidable (∀ e ∈ cache, π e.1 = e.2)) + +omit [DecidableEq α] in +@[simp] theorem agreesWith_nil (π : Equiv.Perm α) : AgreesWith ([] : Cache α) π := + fun _ h => False.elim (List.not_mem_nil h) + +omit [DecidableEq α] in +@[simp] theorem agreesWith_cons (e : α × α) (cache : Cache α) (π : Equiv.Perm α) : + AgreesWith (e :: cache) π ↔ π e.1 = e.2 ∧ AgreesWith cache π := + List.forall_mem_cons + +theorem AgreesWith.apply_of_lookup_eq_some {cache : Cache α} {π : Equiv.Perm α} + (hπ : AgreesWith cache π) {x y : α} (h : cache.lookup x = some y) : + π x = y := + hπ (x, y) (mem_of_lookup_eq_some h) + +theorem AgreesWith.symm_apply_of_invLookup_eq_some {cache : Cache α} {π : Equiv.Perm α} + (hπ : AgreesWith cache π) {y x : α} (h : invLookup cache y = some x) : + π.symm y = x := by + have hxy := hπ (x, y) (mem_of_invLookup_eq_some h) + exact π.symm_apply_eq.mpr hxy.symm + +theorem AgreesWith.invLookup_apply_eq_none {cache : Cache α} {π : Equiv.Perm α} + (hπ : AgreesWith cache π) {x : α} (hx : cache.lookup x = none) : + invLookup cache (π x) = none := by + rw [invLookup_eq_none_iff] + intro e he heq + have h1 : π e.1 = π x := (hπ e he).trans heq + exact lookup_eq_none_iff.mp hx e he (π.injective h1) + +theorem AgreesWith.lookup_symm_apply_eq_none {cache : Cache α} {π : Equiv.Perm α} + (hπ : AgreesWith cache π) {y : α} (hy : invLookup cache y = none) : + cache.lookup (π.symm y) = none := by + rw [lookup_eq_none_iff] + intro e he heq + have h1 : e.2 = y := by + rw [← hπ e he, heq, Equiv.apply_symm_apply] + exact invLookup_eq_none_iff.mp hy e he h1 + +theorem AgreesWith.trans_swap_of_lookup_eq_none {cache : Cache α} {π : Equiv.Perm α} + (hπ : AgreesWith cache π) {x y : α} (hx : cache.lookup x = none) + (hy : invLookup cache y = none) : + AgreesWith ((x, y) :: cache) (π.trans (Equiv.swap (π x) y)) := by + rw [agreesWith_cons] + refine ⟨by simp, fun e he => ?_⟩ + have hne1 : e.2 ≠ π x := by + rw [← hπ e he] + exact fun h => lookup_eq_none_iff.mp hx e he (π.injective h) + have hne2 : e.2 ≠ y := invLookup_eq_none_iff.mp hy e he + simp [hπ e he, Equiv.swap_apply_of_ne_of_ne hne1 hne2] + +theorem AgreesWith.swap_trans_of_invLookup_eq_none {cache : Cache α} {π : Equiv.Perm α} + (hπ : AgreesWith cache π) {x y : α} (hx : cache.lookup x = none) + (hy : invLookup cache y = none) : + AgreesWith ((x, y) :: cache) ((Equiv.swap (π.symm y) x).trans π) := by + rw [agreesWith_cons] + refine ⟨by simp, fun e he => ?_⟩ + have hne1 : e.1 ≠ π.symm y := by + intro h + have h2 : e.2 = y := by rw [← hπ e he, h, Equiv.apply_symm_apply] + exact invLookup_eq_none_iff.mp hy e he h2 + have hne2 : e.1 ≠ x := lookup_eq_none_iff.mp hx e he + rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne hne1 hne2, hπ e he] + +/-- A cache is a partial bijection when at least one permutation on `α` extends it. -/ +def IsPartialBijection (cache : Cache α) : Prop := + ∃ π : Equiv.Perm α, AgreesWith cache π + +omit [DecidableEq α] in +theorem isPartialBijection_nil : IsPartialBijection ([] : Cache α) := + ⟨1, agreesWith_nil 1⟩ + +theorem IsPartialBijection.cons_of_lookup_eq_none {cache : Cache α} + (h : IsPartialBijection cache) {x y : α} (hx : cache.lookup x = none) + (hy : invLookup cache y = none) : + IsPartialBijection ((x, y) :: cache) := by + obtain ⟨π, hπ⟩ := h + exact ⟨π.trans (Equiv.swap (π x) y), hπ.trans_swap_of_lookup_eq_none hx hy⟩ + +/-! ### Finite domain/range complements and extension finsets -/ + +section Finite + +variable [Fintype α] + +/-- Elements of `α` not yet present in the domain of `cache`. -/ +def unusedDomain (cache : Cache α) : Finset α := + Finset.univ.filter fun x => cache.lookup x = none + +/-- Elements of `α` not yet present in the range of `cache`. -/ +def unusedRange (cache : Cache α) : Finset α := + Finset.univ.filter fun y => invLookup cache y = none + +/-- Permutations `π : Equiv.Perm α` that agree with every entry in `cache`. -/ +def extPerms (cache : Cache α) : Finset (Equiv.Perm α) := + Finset.univ.filter fun π => AgreesWith cache π + +@[simp] theorem mem_unusedDomain_iff {cache : Cache α} {x : α} : + x ∈ unusedDomain cache ↔ cache.lookup x = none := by + simp [unusedDomain] + +@[simp] theorem mem_unusedRange_iff {cache : Cache α} {y : α} : + y ∈ unusedRange cache ↔ invLookup cache y = none := by + simp [unusedRange] + +@[simp] theorem mem_extPerms_iff {cache : Cache α} {π : Equiv.Perm α} : + π ∈ extPerms cache ↔ AgreesWith cache π := by + simp [extPerms] + +@[simp] theorem extPerms_nil : extPerms ([] : Cache α) = Finset.univ := by + ext π + simp + +theorem extPerms_nonempty_iff {cache : Cache α} : + (extPerms cache).Nonempty ↔ IsPartialBijection cache := by + simp [Finset.Nonempty, IsPartialBijection] + +theorem IsPartialBijection.unusedRange_nonempty {cache : Cache α} + (h : IsPartialBijection cache) {x : α} (hx : cache.lookup x = none) : + (unusedRange cache).Nonempty := by + obtain ⟨π, hπ⟩ := h + exact ⟨π x, mem_unusedRange_iff.mpr (hπ.invLookup_apply_eq_none hx)⟩ + +theorem IsPartialBijection.unusedDomain_nonempty {cache : Cache α} + (h : IsPartialBijection cache) {y : α} (hy : invLookup cache y = none) : + (unusedDomain cache).Nonempty := by + obtain ⟨π, hπ⟩ := h + exact ⟨π.symm y, mem_unusedDomain_iff.mpr (hπ.lookup_symm_apply_eq_none hy)⟩ + +/-- Post-composing with `Equiv.swap y₁ y₂` bijects extensions of `(x, y₁) :: cache` onto +extensions of `(x, y₂) :: cache` whenever `y₁, y₂ ∈ unusedRange cache`. -/ +private theorem card_extPerms_cons_eq_of_unusedRange {cache : Cache α} (x : α) + {y₁ y₂ : α} (hy₁ : y₁ ∈ unusedRange cache) (hy₂ : y₂ ∈ unusedRange cache) : + (extPerms ((x, y₁) :: cache)).card = (extPerms ((x, y₂) :: cache)).card := by + have hy₁' := mem_unusedRange_iff.mp hy₁ + have hy₂' := mem_unusedRange_iff.mp hy₂ + refine Finset.card_bij (fun π _ => π.trans (Equiv.swap y₁ y₂)) ?_ ?_ ?_ + · intro π hπ + obtain ⟨hπx, hπc⟩ := (agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp hπ) + rw [mem_extPerms_iff, agreesWith_cons] + refine ⟨by simp [hπx], fun e he => ?_⟩ + have h1 : e.2 ≠ y₁ := invLookup_eq_none_iff.mp hy₁' e he + have h2 : e.2 ≠ y₂ := invLookup_eq_none_iff.mp hy₂' e he + simp [hπc e he, Equiv.swap_apply_of_ne_of_ne h1 h2] + · intro π₁ _ π₂ _ heq + ext z + have hz := Equiv.congr_fun heq z + simpa using (Equiv.swap y₁ y₂).injective hz + · intro π hπ + obtain ⟨hπx, hπc⟩ := (agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp hπ) + refine ⟨π.trans (Equiv.swap y₁ y₂), ?_, ?_⟩ + · rw [mem_extPerms_iff, agreesWith_cons] + refine ⟨by simp [hπx], fun e he => ?_⟩ + have h1 : e.2 ≠ y₁ := invLookup_eq_none_iff.mp hy₁' e he + have h2 : e.2 ≠ y₂ := invLookup_eq_none_iff.mp hy₂' e he + simp [hπc e he, Equiv.swap_apply_of_ne_of_ne h1 h2] + · ext z + simp + +/-- Pre-composing with `Equiv.swap x₁ x₂` bijects extensions of `(x₁, y) :: cache` onto +extensions of `(x₂, y) :: cache` whenever `x₁, x₂ ∈ unusedDomain cache`. -/ +private theorem card_extPerms_cons_eq_of_unusedDomain {cache : Cache α} (y : α) + {x₁ x₂ : α} (hx₁ : x₁ ∈ unusedDomain cache) (hx₂ : x₂ ∈ unusedDomain cache) : + (extPerms ((x₁, y) :: cache)).card = (extPerms ((x₂, y) :: cache)).card := by + have hx₁' := mem_unusedDomain_iff.mp hx₁ + have hx₂' := mem_unusedDomain_iff.mp hx₂ + refine Finset.card_bij (fun π _ => (Equiv.swap x₁ x₂).trans π) ?_ ?_ ?_ + · intro π hπ + obtain ⟨hπx, hπc⟩ := (agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp hπ) + rw [mem_extPerms_iff, agreesWith_cons] + refine ⟨by simp [hπx], fun e he => ?_⟩ + have h1 : e.1 ≠ x₁ := lookup_eq_none_iff.mp hx₁' e he + have h2 : e.1 ≠ x₂ := lookup_eq_none_iff.mp hx₂' e he + rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne h1 h2, hπc e he] + · intro π₁ _ π₂ _ heq + ext z + have hz := Equiv.congr_fun heq (Equiv.swap x₁ x₂ z) + simpa using hz + · intro π hπ + obtain ⟨hπx, hπc⟩ := (agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp hπ) + refine ⟨(Equiv.swap x₁ x₂).trans π, ?_, ?_⟩ + · rw [mem_extPerms_iff, agreesWith_cons] + refine ⟨by simp [hπx], fun e he => ?_⟩ + have h1 : e.1 ≠ x₁ := lookup_eq_none_iff.mp hx₁' e he + have h2 : e.1 ≠ x₂ := lookup_eq_none_iff.mp hx₂' e he + rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne h1 h2, hπc e he] + · ext z + simp + +/-- Partitioning `extPerms cache` by the image `π x` of a fresh input `x` shows that all fibers over +`unusedRange cache` have equal size. -/ +theorem card_extPerms_eq_card_unusedRange_mul {cache : Cache α} {x y : α} + (hx : cache.lookup x = none) (hy : y ∈ unusedRange cache) : + (extPerms cache).card = (unusedRange cache).card * (extPerms ((x, y) :: cache)).card := by + have hmaps : ∀ π ∈ extPerms cache, π x ∈ unusedRange cache := fun π hπ => + mem_unusedRange_iff.mpr ((mem_extPerms_iff.mp hπ).invLookup_apply_eq_none hx) + rw [Finset.card_eq_sum_card_fiberwise hmaps] + have hfiber (y' : α) (hy' : y' ∈ unusedRange cache) : + {π ∈ extPerms cache | π x = y'}.card = (extPerms ((x, y) :: cache)).card := by + have hset : {π ∈ extPerms cache | π x = y'} = extPerms ((x, y') :: cache) := by + ext π + simp [And.comm] + rw [hset] + exact card_extPerms_cons_eq_of_unusedRange x hy' hy + rw [Finset.sum_congr rfl hfiber, Finset.sum_const, smul_eq_mul] + +/-- Partitioning `extPerms cache` by the preimage `π.symm y` of a fresh output `y` shows that all +fibers over `unusedDomain cache` have equal size. -/ +theorem card_extPerms_eq_card_unusedDomain_mul {cache : Cache α} {x y : α} + (hx : x ∈ unusedDomain cache) (hy : invLookup cache y = none) : + (extPerms cache).card = (unusedDomain cache).card * (extPerms ((x, y) :: cache)).card := by + have hmaps : ∀ π ∈ extPerms cache, π.symm y ∈ unusedDomain cache := fun π hπ => + mem_unusedDomain_iff.mpr ((mem_extPerms_iff.mp hπ).lookup_symm_apply_eq_none hy) + rw [Finset.card_eq_sum_card_fiberwise hmaps] + have hfiber (x' : α) (hx' : x' ∈ unusedDomain cache) : + {π ∈ extPerms cache | π.symm y = x'}.card = (extPerms ((x, y) :: cache)).card := by + have hset : {π ∈ extPerms cache | π.symm y = x'} = extPerms ((x', y) :: cache) := by + ext π + simp only [Finset.mem_filter, mem_extPerms_iff, agreesWith_cons, Equiv.symm_apply_eq] + exact ⟨fun ⟨h1, h2⟩ => ⟨h2.symm, h1⟩, fun ⟨h2, h1⟩ => ⟨h1, h2.symm⟩⟩ + rw [hset] + exact card_extPerms_cons_eq_of_unusedDomain y hx' hx + rw [Finset.sum_congr rfl hfiber, Finset.sum_const, smul_eq_mul] + +/-! ### Exact lazy bidirectional permutation sampler and eager/lazy equivalence -/ + +variable [Nonempty α] + +/-- Exact without-replacement lazy bidirectional permutation oracle: return cached answers on hits, +and sample uniformly from `unusedRange cache` (for `.forward`) or `unusedDomain cache` (for +`.inverse`) on misses. -/ +noncomputable def answer (q : PermQuery α) : StateT (Cache α) PMF α := fun cache => + match q with + | .forward x => + match cache.lookup x with + | some y => PMF.pure (y, cache) + | none => + if h : (unusedRange cache).Nonempty then + (PMF.uniformOfFinset (unusedRange cache) h).map fun y => (y, (x, y) :: cache) + else + (PMF.uniformOfFintype α).map fun y => (y, (x, y) :: cache) + | .inverse y => + match invLookup cache y with + | some x => PMF.pure (x, cache) + | none => + if h : (unusedDomain cache).Nonempty then + (PMF.uniformOfFinset (unusedDomain cache) h).map fun x => (x, (x, y) :: cache) + else + (PMF.uniformOfFintype α).map fun x => (x, (x, y) :: cache) + +/-- Uniformly sample a full permutation `π : Equiv.Perm α` extending `cache`. -/ +noncomputable def complete (cache : Cache α) : PMF (Equiv.Perm α) := + if h : (extPerms cache).Nonempty then + PMF.uniformOfFinset (extPerms cache) h + else + PMF.uniformOfFintype (Equiv.Perm α) + +omit [Nonempty α] in +/-- Completing the empty cache samples a uniformly random permutation on `α`. -/ +@[simp] theorem complete_nil : + complete ([] : Cache α) = PMF.uniformOfFintype (Equiv.Perm α) := by + ext π + simp [complete, PMF.uniformOfFinset_apply, PMF.uniformOfFintype_apply] + +/-- `answer` preserves `IsPartialBijection` on every supported transition. -/ +theorem answer_preserve_isPartialBijection (q : PermQuery α) (cache : Cache α) + (hcache : IsPartialBijection cache) (a : α) (cache' : Cache α) + (hmem : (a, cache') ∈ (answer q cache).support) : + IsPartialBijection cache' := by + cases q with + | forward x => + dsimp [answer] at hmem + cases hx : cache.lookup x with + | some y => + rw [hx, PMF.mem_support_pure_iff] at hmem + exact (Prod.mk.inj hmem).2 ▸ hcache + | none => + have hne := hcache.unusedRange_nonempty hx + rw [hx, dite_eq_left hne, PMF.mem_support_map_iff] at hmem + obtain ⟨y, hy, heq⟩ := hmem + rw [PMF.mem_support_uniformOfFinset_iff, mem_unusedRange_iff] at hy + obtain ⟨_, rfl⟩ := Prod.mk.inj heq + exact hcache.cons_of_lookup_eq_none hx hy + | inverse y => + dsimp [answer] at hmem + cases hy : invLookup cache y with + | some x => + rw [hy, PMF.mem_support_pure_iff] at hmem + exact (Prod.mk.inj hmem).2 ▸ hcache + | none => + have hne := hcache.unusedDomain_nonempty hy + rw [hy, dite_eq_left hne, PMF.mem_support_map_iff] at hmem + obtain ⟨x, hx, heq⟩ := hmem + rw [PMF.mem_support_uniformOfFinset_iff, mem_unusedDomain_iff] at hx + obtain ⟨_, rfl⟩ := Prod.mk.inj heq + exact hcache.cons_of_lookup_eq_none hx hy + +private theorem map_pair_apply {β γ : Type*} [DecidableEq β] + (p : PMF γ) (f : γ → β) (b : β) (c : γ) : + (p.map fun x => (f x, x)) (b, c) = if b = f c then p c else 0 := by + classical + rw [PMF.map_apply, tsum_eq_single c] + · simp + · intro x hxc + exact ite_eq_right (fun h => hxc (Prod.mk.inj h).2.symm) + +/-- Answering one bidirectional query lazily and then completing the partial bijection has the exact +same joint distribution on `(answer, π)` as completing first and evaluating `evalPerm π q`. -/ +theorem answer_complete (q : PermQuery α) (cache : Cache α) (hcache : IsPartialBijection cache) : + (answer q cache).bind (fun (a, cache') => (complete cache').map (a, ·)) = + (complete cache).map (fun π => (evalPerm π q, π)) := by + have hext_ne : (extPerms cache).Nonempty := extPerms_nonempty_iff.mpr hcache + cases q with + | forward x => + dsimp [answer] + cases hx : cache.lookup x with + | some y => + simp only [PMF.pure_bind] + ext ⟨a, π⟩ + rw [map_pair_apply, map_pair_apply] + by_cases hmem : π ∈ extPerms cache + · have hπx : π x = y := (mem_extPerms_iff.mp hmem).apply_of_lookup_eq_some hx + simp [hπx] + · have hzero : complete cache π = 0 := by + simp [complete, dite_eq_left hext_ne, PMF.uniformOfFinset_apply, hmem] + simp [hzero] + | none => + have hne := hcache.unusedRange_nonempty hx + simp only [dite_eq_left hne, PMF.bind_map, Function.comp_def] + ext ⟨a, π⟩ + rw [map_pair_apply, PMF.bind_apply] + have hterm (y : α) : + PMF.uniformOfFinset (unusedRange cache) hne y * + ((complete ((x, y) :: cache)).map (y, ·)) (a, π) = + if y = a then + PMF.uniformOfFinset (unusedRange cache) hne a * complete ((x, a) :: cache) π + else 0 := by + rw [map_pair_apply] + by_cases hya : y = a + · subst hya; simp + · simp [hya, Ne.symm hya] + simp_rw [hterm, tsum_ite_eq] + by_cases hπ : π ∈ extPerms cache ∧ a = π x + · obtain ⟨hπ_mem, rfl⟩ := hπ + have ha : π x ∈ unusedRange cache := + mem_unusedRange_iff.mpr ((mem_extPerms_iff.mp hπ_mem).invLookup_apply_eq_none hx) + have hcons_mem : π ∈ extPerms ((x, π x) :: cache) := by + rw [mem_extPerms_iff, agreesWith_cons] + exact ⟨rfl, mem_extPerms_iff.mp hπ_mem⟩ + have hcons_ne : (extPerms ((x, π x) :: cache)).Nonempty := ⟨π, hcons_mem⟩ + rw [complete, dite_eq_left hcons_ne, complete, dite_eq_left hext_ne] + simp only [PMF.uniformOfFinset_apply, ha, hcons_mem, hπ_mem, ↓reduceIte] + rw [card_extPerms_eq_card_unusedRange_mul hx ha, Nat.cast_mul, + ENNReal.mul_inv (Or.inl (Nat.cast_ne_zero.mpr hne.card_pos.ne')) + (Or.inl (ENNReal.natCast_ne_top _))] + · rw [not_and_or] at hπ + rcases hπ with hπ_not | hne_ax + · have h0 : complete cache π = 0 := by + simp [complete, dite_eq_left hext_ne, PMF.uniformOfFinset_apply, hπ_not] + rw [h0, ite_self] + by_cases ha : a ∈ unusedRange cache + · have hcons_ne : (extPerms ((x, a) :: cache)).Nonempty := + extPerms_nonempty_iff.mpr + (hcache.cons_of_lookup_eq_none hx (mem_unusedRange_iff.mp ha)) + have hnot_cons : π ∉ extPerms ((x, a) :: cache) := fun h => + hπ_not (mem_extPerms_iff.mpr ((agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp h)).2) + simp [complete, dite_eq_left hcons_ne, PMF.uniformOfFinset_apply, hnot_cons] + · simp [PMF.uniformOfFinset_apply, ha] + · simp only [hne_ax, ↓reduceIte] + by_cases ha : a ∈ unusedRange cache + · have hcons_ne : (extPerms ((x, a) :: cache)).Nonempty := + extPerms_nonempty_iff.mpr + (hcache.cons_of_lookup_eq_none hx (mem_unusedRange_iff.mp ha)) + have hnot_cons : π ∉ extPerms ((x, a) :: cache) := fun h => + hne_ax ((agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp h)).1.symm + simp [complete, dite_eq_left hcons_ne, PMF.uniformOfFinset_apply, hnot_cons] + · simp [PMF.uniformOfFinset_apply, ha] + | inverse y => + dsimp [answer] + cases hy : invLookup cache y with + | some x => + simp only [PMF.pure_bind] + ext ⟨a, π⟩ + rw [map_pair_apply, map_pair_apply] + by_cases hmem : π ∈ extPerms cache + · have hπy : π.symm y = x := (mem_extPerms_iff.mp hmem).symm_apply_of_invLookup_eq_some hy + simp [hπy] + · have hzero : complete cache π = 0 := by + simp [complete, dite_eq_left hext_ne, PMF.uniformOfFinset_apply, hmem] + simp [hzero] + | none => + have hne := hcache.unusedDomain_nonempty hy + simp only [dite_eq_left hne, PMF.bind_map, Function.comp_def] + ext ⟨a, π⟩ + rw [map_pair_apply, PMF.bind_apply] + have hterm (x : α) : + PMF.uniformOfFinset (unusedDomain cache) hne x * + ((complete ((x, y) :: cache)).map (x, ·)) (a, π) = + if x = a then + PMF.uniformOfFinset (unusedDomain cache) hne a * complete ((a, y) :: cache) π + else 0 := by + rw [map_pair_apply] + by_cases hxa : x = a + · subst hxa; simp + · simp [hxa, Ne.symm hxa] + simp_rw [hterm, tsum_ite_eq] + by_cases hπ : π ∈ extPerms cache ∧ a = π.symm y + · obtain ⟨hπ_mem, rfl⟩ := hπ + have ha : π.symm y ∈ unusedDomain cache := + mem_unusedDomain_iff.mpr ((mem_extPerms_iff.mp hπ_mem).lookup_symm_apply_eq_none hy) + have hcons_mem : π ∈ extPerms ((π.symm y, y) :: cache) := by + rw [mem_extPerms_iff, agreesWith_cons] + exact ⟨Equiv.apply_symm_apply π y, mem_extPerms_iff.mp hπ_mem⟩ + have hcons_ne : (extPerms ((π.symm y, y) :: cache)).Nonempty := ⟨π, hcons_mem⟩ + rw [complete, dite_eq_left hcons_ne, complete, dite_eq_left hext_ne] + simp only [PMF.uniformOfFinset_apply, ha, hcons_mem, hπ_mem, ↓reduceIte] + rw [card_extPerms_eq_card_unusedDomain_mul ha hy, Nat.cast_mul, + ENNReal.mul_inv (Or.inl (Nat.cast_ne_zero.mpr hne.card_pos.ne')) + (Or.inl (ENNReal.natCast_ne_top _))] + · rw [not_and_or] at hπ + rcases hπ with hπ_not | hne_ay + · have h0 : complete cache π = 0 := by + simp [complete, dite_eq_left hext_ne, PMF.uniformOfFinset_apply, hπ_not] + rw [h0, ite_self] + by_cases ha : a ∈ unusedDomain cache + · have hcons_ne : (extPerms ((a, y) :: cache)).Nonempty := + extPerms_nonempty_iff.mpr + (hcache.cons_of_lookup_eq_none (mem_unusedDomain_iff.mp ha) hy) + have hnot_cons : π ∉ extPerms ((a, y) :: cache) := fun h => + hπ_not (mem_extPerms_iff.mpr ((agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp h)).2) + simp [complete, dite_eq_left hcons_ne, PMF.uniformOfFinset_apply, hnot_cons] + · simp [PMF.uniformOfFinset_apply, ha] + · simp only [hne_ay, ↓reduceIte] + by_cases ha : a ∈ unusedDomain cache + · have hcons_ne : (extPerms ((a, y) :: cache)).Nonempty := + extPerms_nonempty_iff.mpr + (hcache.cons_of_lookup_eq_none (mem_unusedDomain_iff.mp ha) hy) + have hnot_cons : π ∉ extPerms ((a, y) :: cache) := fun h => + hne_ay (π.symm_apply_eq.mpr + ((agreesWith_cons _ _ _).mp (mem_extPerms_iff.mp h)).1.symm).symm + simp [complete, dite_eq_left hcons_ne, PMF.uniformOfFinset_apply, hnot_cons] + · simp [PMF.uniformOfFinset_apply, ha] + +/-- **Eager/lazy equivalence for bidirectional permutations**: running an adaptive program against +`answer` from any partial bijection `cache` and then completing `cache'` to a full permutation gives +the same joint distribution on `(result, π)` as completing `cache` first and answering queries via +`evalPerm π`. -/ +theorem run_interpret_answer_complete {β : Type} + (program : OracleComp (PermOracleSpec α) β) (cache : Cache α) + (hcache : IsPartialBijection cache) : + (do + let (result, cache') ← (OracleComp.interpret answer program).run cache + (complete cache').map (result, ·)) = + (do + let π ← complete cache + (OracleComp.interpret (fun q => PMF.pure (evalPerm π q)) program).map (·, π)) := by + simp only [PMF.monad_bind_eq_bind] + have h := OracleComp.run_interpret_simulation_of_invariant answer + (fun q π => (·, π) <$> PMF.pure (evalPerm π q)) complete IsPartialBijection + answer_preserve_isPartialBijection + (fun q c hc => by + simpa only [PMF.monad_bind_eq_bind, PMF.monad_map_eq_map, PMF.pure_map, PMF.map, + Function.comp_def, PMF.pure_bind] using answer_complete q c hc) + program cache hcache + refine h.trans (congrArg ((complete cache).bind) (funext fun π => ?_)) + simpa only [PMF.monad_map_eq_map] using OracleComp.run_interpret_readOnly + (fun q (π : Equiv.Perm α) => PMF.pure (evalPerm π q)) program π + +/-- **Uniform random permutation equals lazy bidirectional sampling**: sampling a uniform +permutation `π ← PMF.uniformOfFintype (Equiv.Perm α)` and answering bidirectional queries via +`evalPerm π` has the exact same output distribution as running `answer` from the empty cache +`[]`. -/ +theorem uniform_interpret_eq_lazy {β : Type} (program : OracleComp (PermOracleSpec α) β) : + (do + let π ← PMF.uniformOfFintype (Equiv.Perm α) + OracleComp.interpret (fun q => PMF.pure (evalPerm π q)) program) = + ((OracleComp.interpret answer program).run []).map Prod.fst := by + have h := congrArg (PMF.map Prod.fst) + (run_interpret_answer_complete program [] isPartialBijection_nil) + simpa only [PMF.monad_bind_eq_bind, complete_nil, PMF.map_bind, PMF.map_comp, PMF.map, + Function.comp_def, PMF.bind_const, PMF.bind_pure, PMF.bind_bind, PMF.pure_bind] using h.symm + +/-! ### Forgetful lazy permutation sampler and bidirectional switching bound -/ + +/-- **Forgetful lazy bidirectional permutation oracle** ([BonehShoup2023], Section 4.7): return the +cached image/preimage on a hit, and sample uniformly from all of `α` (with replacement) on a +miss. -/ +noncomputable def forgetfulAnswer (q : PermQuery α) : StateT (Cache α) PMF α := fun cache => + match q with + | .forward x => + match cache.lookup x with + | some y => PMF.pure (y, cache) + | none => (PMF.uniformOfFintype α).map fun y => (y, (x, y) :: cache) + | .inverse y => + match invLookup cache y with + | some x => PMF.pure (x, cache) + | none => (PMF.uniformOfFintype α).map fun x => (x, (x, y) :: cache) + +/-- On forward-only programs (`liftForward`), `forgetfulAnswer` never queries `invLookup`, so its +joint result and cache distribution is identical to `memoize (fun _ => PMF.uniformOfFintype α)`. -/ +theorem run_interpret_forgetfulAnswer_liftForward {β : Type} + (program : OracleComp (fun _ : α => α) β) (cache : Cache α) : + (OracleComp.interpret forgetfulAnswer (liftForward program)).run cache = + (OracleComp.interpret (memoize (fun _ : α => PMF.uniformOfFintype α)) program).run cache := by + rw [liftForward, OracleComp.interpret_interpret] + congr 2 + funext x c + cases h : c.lookup x <;> + simp [forgetfulAnswer, h, memoize_of_none, memoize_of_some, PMF.map, Function.comp_def, + PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure] + +/-- Forgetful lazy handler instrumented with a `bad` flag that records whether a fresh forward draw +collided with `ran(cache)` or a fresh inverse draw collided with `dom(cache)`. -/ +private noncomputable def forgetfulWithBad (q : PermQuery α) : + StateT (Cache α × Bool) PMF α := fun (cache, bad) => + match q with + | .forward x => + match cache.lookup x with + | some y => PMF.pure (y, (cache, bad)) + | none => + (PMF.uniformOfFintype α).map fun y => + (y, ((x, y) :: cache, bad || (invLookup cache y).isSome)) + | .inverse y => + match invLookup cache y with + | some x => PMF.pure (x, (cache, bad)) + | none => + (PMF.uniformOfFintype α).map fun x => + (x, ((x, y) :: cache, bad || (cache.lookup x).isSome)) + +/-- Coupled exact lazy handler with a `bad` flag: draw a candidate uniformly from `α`; if it lies in +`unusedRange` (resp. `unusedDomain`), use it directly, and otherwise set `bad := true` and resample +uniformly from `unusedRange` (resp. `unusedDomain`). -/ +private noncomputable def exactWithBad (q : PermQuery α) : + StateT (Cache α × Bool) PMF α := fun (cache, bad) => + match q with + | .forward x => + match cache.lookup x with + | some y => PMF.pure (y, (cache, bad)) + | none => do + let y₀ ← PMF.uniformOfFintype α + if (invLookup cache y₀).isSome then + (answer (.forward x) cache).map fun (y, cache') => (y, (cache', true)) + else + PMF.pure (y₀, ((x, y₀) :: cache, bad)) + | .inverse y => + match invLookup cache y with + | some x => PMF.pure (x, (cache, bad)) + | none => do + let x₀ ← PMF.uniformOfFintype α + if (cache.lookup x₀).isSome then + (answer (.inverse y) cache).map fun (x, cache') => (x, (cache', true)) + else + PMF.pure (x₀, ((x₀, y) :: cache, bad)) + +private theorem forgetfulWithBad_map_fst (q : PermQuery α) (st : Cache α × Bool) : + (forgetfulWithBad q st).map (fun (a, st') => (a, st'.1)) = forgetfulAnswer q st.1 := by + rcases st with ⟨cache, bad⟩ + cases q with + | forward x => + cases h : cache.lookup x <;> + simp [forgetfulWithBad, forgetfulAnswer, h, PMF.pure_map, PMF.map_comp, Function.comp_def] + | inverse y => + cases h : invLookup cache y <;> + simp [forgetfulWithBad, forgetfulAnswer, h, PMF.pure_map, PMF.map_comp, Function.comp_def] + +private theorem run_interpret_forgetfulWithBad_map_fst {β : Type} + (program : OracleComp (PermOracleSpec α) β) (cache : Cache α) (bad : Bool) : + ((OracleComp.interpret forgetfulWithBad program).run (cache, bad)).map + (fun (a, st') => (a, st'.1)) = + (OracleComp.interpret forgetfulAnswer program).run cache := + OracleComp.run_interpret_map_state forgetfulWithBad forgetfulAnswer Prod.fst + forgetfulWithBad_map_fst program (cache, bad) + +/-- **Finite-set resampling identity**: drawing `a₀ ← PMF.uniformOfFintype α` and returning `a₀` if +`a₀ ∈ S` or resampling from `PMF.uniformOfFinset S hS` if `a₀ ∉ S` produces +`PMF.uniformOfFinset S hS`. -/ +private theorem uniformOfFintype_bind_ite_uniformOfFinset (S : Finset α) (hS : S.Nonempty) : + ((PMF.uniformOfFintype α).bind fun a₀ => + if a₀ ∈ S then PMF.pure a₀ else PMF.uniformOfFinset S hS) = + PMF.uniformOfFinset S hS := by + ext a + rw [PMF.bind_apply, tsum_fintype, PMF.uniformOfFinset_apply] + by_cases ha : a ∈ S + · simp only [ha, ↓reduceIte] + have hsplit : + (∑ a₀ : α, PMF.uniformOfFintype α a₀ * + (if a₀ ∈ S then PMF.pure a₀ else PMF.uniformOfFinset S hS) a) = + (∑ a₀ ∈ S, PMF.uniformOfFintype α a₀ * PMF.pure a₀ a) + + (∑ a₀ ∈ Sᶜ, PMF.uniformOfFintype α a₀ * PMF.uniformOfFinset S hS a) := by + rw [← Finset.sum_add_sum_compl S] + congr 1 + · refine Finset.sum_congr rfl fun a₀ ha₀ => by simp [ha₀] + · refine Finset.sum_congr rfl fun a₀ ha₀ => by + rw [Finset.mem_compl] at ha₀ + simp [ha₀] + rw [hsplit] + have h1 : (∑ a₀ ∈ S, PMF.uniformOfFintype α a₀ * PMF.pure a₀ a) = + (Fintype.card α : ℝ≥0∞)⁻¹ := by + have hterm (a₀ : α) : PMF.uniformOfFintype α a₀ * PMF.pure a₀ a = + if a₀ = a then (Fintype.card α : ℝ≥0∞)⁻¹ else 0 := by + by_cases h0 : a₀ = a + · subst h0; simp [PMF.uniformOfFintype_apply] + · simp [PMF.pure_apply, h0, Ne.symm h0] + simp_rw [hterm] + rw [Finset.sum_ite_eq' S a, ite_eq_left ha] + have h2 : (∑ a₀ ∈ Sᶜ, PMF.uniformOfFintype α a₀ * PMF.uniformOfFinset S hS a) = + (Sᶜ.card : ℝ≥0∞) * (Fintype.card α : ℝ≥0∞)⁻¹ * (S.card : ℝ≥0∞)⁻¹ := by + simp only [PMF.uniformOfFintype_apply, PMF.uniformOfFinset_apply, ha, ↓reduceIte, + Finset.sum_const, nsmul_eq_mul, mul_assoc] + rw [h1, h2] + have hcard : (S.card : ℝ≥0∞) + Sᶜ.card = Fintype.card α := by + exact_mod_cast Finset.card_add_card_compl S + have hS_ne : (S.card : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.mpr hS.card_pos.ne' + have hS_top : (S.card : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _ + have hα_ne : (Fintype.card α : ℝ≥0∞) ≠ 0 := Nat.cast_ne_zero.mpr Fintype.card_ne_zero + have hα_top : (Fintype.card α : ℝ≥0∞) ≠ ⊤ := ENNReal.natCast_ne_top _ + calc (Fintype.card α : ℝ≥0∞)⁻¹ + + (Sᶜ.card : ℝ≥0∞) * (Fintype.card α : ℝ≥0∞)⁻¹ * (S.card : ℝ≥0∞)⁻¹ + = (S.card : ℝ≥0∞) * (S.card : ℝ≥0∞)⁻¹ * (Fintype.card α : ℝ≥0∞)⁻¹ + + (Sᶜ.card : ℝ≥0∞) * (Fintype.card α : ℝ≥0∞)⁻¹ * (S.card : ℝ≥0∞)⁻¹ := by + rw [ENNReal.mul_inv_cancel hS_ne hS_top, one_mul] + _ = ((S.card : ℝ≥0∞) + Sᶜ.card) * (Fintype.card α : ℝ≥0∞)⁻¹ * (S.card : ℝ≥0∞)⁻¹ := by + ring + _ = (S.card : ℝ≥0∞)⁻¹ := by + rw [hcard, ENNReal.mul_inv_cancel hα_ne hα_top, one_mul] + · simp only [ha, ↓reduceIte] + refine Finset.sum_eq_zero fun a₀ _ => ?_ + by_cases ha₀ : a₀ ∈ S + · have hne : a ≠ a₀ := fun h => ha (h ▸ ha₀) + simp [ha₀, PMF.pure_apply, hne] + · simp [ha₀, PMF.uniformOfFinset_apply, ha] + +private theorem exactWithBad_preserve_isPartialBijection (q : PermQuery α) (st : Cache α × Bool) + (hst : IsPartialBijection st.1) (a : α) (st' : Cache α × Bool) + (hmem : (a, st') ∈ (exactWithBad q st).support) : + IsPartialBijection st'.1 := by + rcases st with ⟨cache, bad⟩ + cases q with + | forward x => + dsimp [exactWithBad, Probability.PMF.monad_bind_eq_bind] at hmem + cases hx : cache.lookup x with + | some y => + rw [hx, PMF.mem_support_pure_iff] at hmem + exact (Prod.mk.inj hmem).2 ▸ hst + | none => + rw [hx, PMF.mem_support_bind_iff] at hmem + obtain ⟨y₀, -, hy₀⟩ := hmem + by_cases his : (invLookup cache y₀).isSome + · rw [ite_eq_left his, PMF.mem_support_map_iff] at hy₀ + obtain ⟨⟨y, cache'⟩, hmem', heq⟩ := hy₀ + obtain ⟨_, rfl⟩ := Prod.mk.inj heq + exact answer_preserve_isPartialBijection (.forward x) cache hst y cache' hmem' + · rw [ite_eq_right his, PMF.mem_support_pure_iff] at hy₀ + obtain ⟨_, rfl⟩ := Prod.mk.inj hy₀ + exact hst.cons_of_lookup_eq_none hx (Option.not_isSome_iff_eq_none.mp his) + | inverse y => + dsimp [exactWithBad, Probability.PMF.monad_bind_eq_bind] at hmem + cases hy : invLookup cache y with + | some x => + rw [hy, PMF.mem_support_pure_iff] at hmem + exact (Prod.mk.inj hmem).2 ▸ hst + | none => + rw [hy, PMF.mem_support_bind_iff] at hmem + obtain ⟨x₀, -, hx₀⟩ := hmem + by_cases his : (cache.lookup x₀).isSome + · rw [ite_eq_left his, PMF.mem_support_map_iff] at hx₀ + obtain ⟨⟨x, cache'⟩, hmem', heq⟩ := hx₀ + obtain ⟨_, rfl⟩ := Prod.mk.inj heq + exact answer_preserve_isPartialBijection (.inverse y) cache hst x cache' hmem' + · rw [ite_eq_right his, PMF.mem_support_pure_iff] at hx₀ + obtain ⟨_, rfl⟩ := Prod.mk.inj hx₀ + exact hst.cons_of_lookup_eq_none (Option.not_isSome_iff_eq_none.mp his) hy + +private theorem exactWithBad_map_fst (q : PermQuery α) (st : Cache α × Bool) + (hst : IsPartialBijection st.1) : + (exactWithBad q st).map (fun (a, st') => (a, st'.1)) = answer q st.1 := by + rcases st with ⟨cache, bad⟩ + cases q with + | forward x => + dsimp [exactWithBad, Probability.PMF.monad_bind_eq_bind] + cases hx : cache.lookup x with + | some y => simp [answer, hx, PMF.pure_map] + | none => + have hne := hst.unusedRange_nonempty hx + have hans : answer (.forward x) cache = + (PMF.uniformOfFinset (unusedRange cache) hne).map fun y => (y, (x, y) :: cache) := by + simp [answer, hx, dite_eq_left hne] + conv_rhs => + rw [hans, ← uniformOfFintype_bind_ite_uniformOfFinset (unusedRange cache) hne, + PMF.map_bind] + rw [PMF.map_bind] + congr 1 + funext y₀ + by_cases hy₀ : y₀ ∈ unusedRange cache + · have his : (invLookup cache y₀).isSome = false := by + rw [Option.isSome_eq_false_iff, Option.isNone_iff_eq_none] + exact mem_unusedRange_iff.mp hy₀ + simp [hy₀, his, PMF.pure_map] + · have his : (invLookup cache y₀).isSome = true := by + rw [← Option.ne_none_iff_isSome] + exact fun h => hy₀ (mem_unusedRange_iff.mpr h) + simp [hy₀, his, hans, PMF.map_comp, Function.comp_def] + | inverse y => + dsimp [exactWithBad, Probability.PMF.monad_bind_eq_bind] + cases hy : invLookup cache y with + | some x => simp [answer, hy, PMF.pure_map] + | none => + have hne := hst.unusedDomain_nonempty hy + have hans : answer (.inverse y) cache = + (PMF.uniformOfFinset (unusedDomain cache) hne).map fun x => (x, (x, y) :: cache) := by + simp [answer, hy, dite_eq_left hne] + conv_rhs => + rw [hans, ← uniformOfFintype_bind_ite_uniformOfFinset (unusedDomain cache) hne, + PMF.map_bind] + rw [PMF.map_bind] + congr 1 + funext x₀ + by_cases hx₀ : x₀ ∈ unusedDomain cache + · have his : (cache.lookup x₀).isSome = false := by + rw [Option.isSome_eq_false_iff, Option.isNone_iff_eq_none] + exact mem_unusedDomain_iff.mp hx₀ + simp [hx₀, his, PMF.pure_map] + · have his : (cache.lookup x₀).isSome = true := by + rw [← Option.ne_none_iff_isSome] + exact fun h => hx₀ (mem_unusedDomain_iff.mpr h) + simp [hx₀, his, hans, PMF.map_comp, Function.comp_def] + +private theorem run_interpret_exactWithBad_map_fst {β : Type} + (program : OracleComp (PermOracleSpec α) β) (cache : Cache α) (bad : Bool) + (hcache : IsPartialBijection cache) : + ((OracleComp.interpret exactWithBad program).run (cache, bad)).map + (fun (a, st') => (a, st'.1)) = + (OracleComp.interpret answer program).run cache := + OracleComp.run_interpret_map_state_of_invariant exactWithBad answer Prod.fst + (fun st => IsPartialBijection st.1) exactWithBad_preserve_isPartialBijection + exactWithBad_map_fst program (cache, bad) hcache + +/-- `exactWithBad` and `forgetfulWithBad` are identical until `bad = true`. -/ +private theorem identicalUntilBad_exactWithBad_forgetfulWithBad : + IdenticalUntilBad (spec := PermOracleSpec α) exactWithBad forgetfulWithBad + (fun st : Cache α × Bool => st.2 = true) where + agree q st hst a st' hst' := by + rcases st with ⟨cache, bad⟩ + rcases st' with ⟨cache', bad'⟩ + have hbad : bad = false := Bool.eq_false_iff.mpr hst + have hbad' : bad' = false := Bool.eq_false_iff.mpr hst' + subst hbad hbad' + cases q with + | forward x => + dsimp [exactWithBad, forgetfulWithBad, Probability.PMF.monad_bind_eq_bind] + cases hx : cache.lookup x with + | some y => rfl + | none => + rw [PMF.bind_apply, PMF.map_apply] + refine tsum_congr fun y₀ => ?_ + by_cases his : (invLookup cache y₀).isSome = true + · rw [ite_eq_left his, his, Bool.false_or] + have h0 : ((answer (.forward x) cache).map fun x => (x.1, x.2, true)) + (a, cache', false) = 0 := by + rw [PMF.apply_eq_zero_iff, PMF.mem_support_map_iff] + rintro ⟨p, -, hp⟩ + exact Bool.noConfusion (Prod.mk.inj (Prod.mk.inj hp).2).2 + have hne : (a, cache', false) ≠ (y₀, (x, y₀) :: cache, true) := fun h => + Bool.noConfusion (Prod.mk.inj (Prod.mk.inj h).2).2 + simp [h0, hne] + · have his' : (invLookup cache y₀).isSome = false := Bool.eq_false_iff.mpr his + rw [ite_eq_right his, his', Bool.false_or, PMF.pure_apply] + by_cases heq : (a, cache', false) = (y₀, (x, y₀) :: cache, false) <;> simp [heq] + | inverse y => + dsimp [exactWithBad, forgetfulWithBad, Probability.PMF.monad_bind_eq_bind] + cases hy : invLookup cache y with + | some x => rfl + | none => + rw [PMF.bind_apply, PMF.map_apply] + refine tsum_congr fun x₀ => ?_ + by_cases his : (cache.lookup x₀).isSome = true + · rw [ite_eq_left his, his, Bool.false_or] + have h0 : ((answer (.inverse y) cache).map fun x => (x.1, x.2, true)) + (a, cache', false) = 0 := by + rw [PMF.apply_eq_zero_iff, PMF.mem_support_map_iff] + rintro ⟨p, -, hp⟩ + exact Bool.noConfusion (Prod.mk.inj (Prod.mk.inj hp).2).2 + have hne : (a, cache', false) ≠ (x₀, (x₀, y) :: cache, true) := fun h => + Bool.noConfusion (Prod.mk.inj (Prod.mk.inj h).2).2 + simp [h0, hne] + · have his' : (cache.lookup x₀).isSome = false := Bool.eq_false_iff.mpr his + rw [ite_eq_right his, his', Bool.false_or, PMF.pure_apply] + by_cases heq : (a, cache', false) = (x₀, (x₀, y) :: cache, false) <;> simp [heq] + absorb_first q st hst p hp := by + rcases st with ⟨cache, bad⟩ + dsimp at hst + subst hst + cases q with + | forward x => + dsimp [exactWithBad, Probability.PMF.monad_bind_eq_bind] at hp + cases hx : cache.lookup x with + | some y => + rw [hx, PMF.mem_support_pure_iff] at hp + rw [hp] + | none => + rw [hx, PMF.mem_support_bind_iff] at hp + obtain ⟨y₀, -, hy₀⟩ := hp + by_cases his : (invLookup cache y₀).isSome + · rw [ite_eq_left his, PMF.mem_support_map_iff] at hy₀ + obtain ⟨_, -, rfl⟩ := hy₀ + rfl + · rw [ite_eq_right his, PMF.mem_support_pure_iff] at hy₀ + rw [hy₀] + | inverse y => + dsimp [exactWithBad, Probability.PMF.monad_bind_eq_bind] at hp + cases hy : invLookup cache y with + | some x => + rw [hy, PMF.mem_support_pure_iff] at hp + rw [hp] + | none => + rw [hy, PMF.mem_support_bind_iff] at hp + obtain ⟨x₀, -, hx₀⟩ := hp + by_cases his : (cache.lookup x₀).isSome + · rw [ite_eq_left his, PMF.mem_support_map_iff] at hx₀ + obtain ⟨_, -, rfl⟩ := hx₀ + rfl + · rw [ite_eq_right his, PMF.mem_support_pure_iff] at hx₀ + rw [hx₀] + absorb_second q st hst p hp := by + rcases st with ⟨cache, bad⟩ + dsimp at hst + subst hst + cases q with + | forward x => + dsimp [forgetfulWithBad] at hp + cases hx : cache.lookup x with + | some y => + rw [hx, PMF.mem_support_pure_iff] at hp + rw [hp] + | none => + rw [hx, PMF.mem_support_map_iff] at hp + obtain ⟨y₀, -, rfl⟩ := hp + simp + | inverse y => + dsimp [forgetfulWithBad] at hp + cases hy : invLookup cache y with + | some x => + rw [hy, PMF.mem_support_pure_iff] at hp + rw [hp] + | none => + rw [hy, PMF.mem_support_map_iff] at hp + obtain ⟨x₀, -, rfl⟩ := hp + simp + +/-! ### Quadratic union bound for linearly growing collision sets -/ + +/-- If each oracle call from a good state `s` turns bad with probability at most `size s * δ` and +increases `size` by at most `1`, then an adaptive program making at most `n` queries reaches a bad +state from `s` with probability at most `(n * size s + n.choose 2) * δ`. -/ +theorem toOuterMeasure_bad_choose_two_le {ι σ β : Type} {spec : ι → Type} + {handler : (q : ι) → StateT σ PMF (spec q)} {bad : σ → Prop} + (size : σ → ℕ) (δ : ℝ≥0∞) + (hstep : ∀ q s, ¬bad s → (handler q s).toOuterMeasure {x | bad x.2} ≤ size s * δ) + (hgrow : ∀ q s, ¬bad s → ∀ x ∈ (handler q s).support, ¬bad x.2 → size x.2 ≤ size s + 1) + {program : OracleComp spec β} {n : ℕ} (hn : IsQueryBounded program n) + {s : σ} (hs : ¬bad s) : + ((OracleComp.interpret handler program).run s).toOuterMeasure {x | bad x.2} ≤ + (n * size s + n.choose 2 : ℕ) * δ := by + induction hn generalizing s with + | pure a n => + simp only [run_interpret_pure, Probability.PMF.monad_pure_eq_pure, + PMF.toOuterMeasure_pure_apply, ite_eq_right (show (a, s) ∉ {x : β × σ | bad x.2} from hs)] + exact zero_le + | liftBind q cont n _ ih => + classical + simp only [run_interpret_bind, run_interpret_query, + Probability.PMF.monad_bind_eq_bind, PMF.toOuterMeasure_bind_apply] + set K : ℝ≥0∞ := (n * (size s + 1) + n.choose 2 : ℕ) * δ + have hterm (y : spec q × σ) : + (handler q s) y * + ((OracleComp.interpret handler (cont y.1)).run y.2).toOuterMeasure {x | bad x.2} ≤ + (handler q s) y * ({x : spec q × σ | bad x.2}.indicator 1 y + K) := by + by_cases hmem : y ∈ (handler q s).support + · refine mul_le_mul_of_nonneg_left ?_ zero_le + by_cases hy : bad y.2 + · have : y ∈ {x : spec q × σ | bad x.2} := hy + rw [Set.indicator_of_mem this, Pi.one_apply] + exact (Probability.PMF.toOuterMeasure_le_one _ _).trans le_self_add + · have : y ∉ {x : spec q × σ | bad x.2} := hy + rw [Set.indicator_of_notMem this, zero_add] + refine (ih y.1 hy).trans ?_ + simp only [K] + gcongr + exact hgrow q s hs y hmem hy + · rw [(PMF.apply_eq_zero_iff _ _).mpr hmem, zero_mul, zero_mul] + calc ∑' y, (handler q s) y * + ((OracleComp.interpret handler (cont y.1)).run y.2).toOuterMeasure {x | bad x.2} + ≤ ∑' y, (handler q s) y * ({x : spec q × σ | bad x.2}.indicator 1 y + K) := + ENNReal.tsum_le_tsum hterm + _ = (handler q s).toOuterMeasure {x | bad x.2} + K := by + simp only [mul_add, ENNReal.tsum_add, ENNReal.tsum_mul_right, PMF.tsum_coe, one_mul, + PMF.toOuterMeasure_apply] + congr 1 + refine tsum_congr fun y => ?_ + by_cases hy : y ∈ {x : spec q × σ | bad x.2} + · rw [Set.indicator_of_mem hy, Set.indicator_of_mem hy, Pi.one_apply, mul_one] + · rw [Set.indicator_of_notMem hy, Set.indicator_of_notMem hy, mul_zero] + _ ≤ size s * δ + K := add_le_add (hstep q s hs) le_rfl + _ = ((n + 1) * size s + (n + 1).choose 2 : ℕ) * δ := by + simp only [K, Nat.choose_succ_succ' n 1, Nat.choose_one_right, Nat.cast_add, + Nat.cast_mul, Nat.cast_one] + ring + +omit [Nonempty α] in +private theorem card_filter_lookup_isSome_le (cache : Cache α) : + (Finset.univ.filter fun x : α => (cache.lookup x).isSome = true).card ≤ cache.length := by + have hsub : (Finset.univ.filter fun x : α => (cache.lookup x).isSome = true) ⊆ + (cache.map Prod.fst).toFinset := by + intro x hx + rw [Finset.mem_filter, Option.isSome_iff_exists] at hx + obtain ⟨_, y, hy⟩ := hx + rw [List.mem_toFinset, List.mem_map] + exact ⟨(x, y), mem_of_lookup_eq_some hy, rfl⟩ + exact (Finset.card_le_card hsub).trans + ((List.toFinset_card_le _).trans (by simp)) + +omit [Nonempty α] in +private theorem card_filter_invLookup_isSome_le (cache : Cache α) : + (Finset.univ.filter fun y : α => (invLookup cache y).isSome = true).card ≤ cache.length := by + simpa [invLookup] using card_filter_lookup_isSome_le (cache.map Prod.swap) + +/-- Over an `n`-query-bounded program starting from `(cache, false)`, `forgetfulWithBad` reaches +`bad = true` with probability at most `(n * cache.length + n.choose 2) * |α|⁻¹`. -/ +private theorem toOuterMeasure_bad_forgetfulWithBad_le {β : Type} + {program : OracleComp (PermOracleSpec α) β} {n : ℕ} + (hn : IsQueryBounded program n) (cache : Cache α) : + ((OracleComp.interpret forgetfulWithBad program).run (cache, false)).toOuterMeasure + {x | x.2.2 = true} ≤ + (n * cache.length + n.choose 2 : ℕ) * (Fintype.card α : ℝ≥0∞)⁻¹ := by + refine toOuterMeasure_bad_choose_two_le (bad := fun st : Cache α × Bool => st.2 = true) + (fun st : Cache α × Bool => st.1.length) + (Fintype.card α : ℝ≥0∞)⁻¹ ?_ ?_ hn Bool.false_ne_true + · intro q ⟨c, b⟩ hb + have hb' : b = false := Bool.eq_false_iff.mpr hb + subst hb' + cases q with + | forward x => + dsimp [forgetfulWithBad] + cases hx : c.lookup x with + | some y => simp [PMF.toOuterMeasure_pure_apply] + | none => + have hpre : (fun y : α => (y, ((x, y) :: c, false || (invLookup c y).isSome))) ⁻¹' + {x : α × (Cache α × Bool) | x.2.2 = true} = + {y : α | (invLookup c y).isSome = true} := by + ext y + simp + rw [PMF.toOuterMeasure_map_apply, hpre, PMF.toOuterMeasure_uniformOfFintype] + gcongr + exact Nat.cast_le.mpr (card_filter_invLookup_isSome_le c) + | inverse y => + dsimp [forgetfulWithBad] + cases hy : invLookup c y with + | some x => simp [PMF.toOuterMeasure_pure_apply] + | none => + have hpre : (fun x : α => (x, ((x, y) :: c, false || (c.lookup x).isSome))) ⁻¹' + {x : α × (Cache α × Bool) | x.2.2 = true} = + {x : α | (c.lookup x).isSome = true} := by + ext x + simp + rw [PMF.toOuterMeasure_map_apply, hpre, PMF.toOuterMeasure_uniformOfFintype] + gcongr + exact Nat.cast_le.mpr (card_filter_lookup_isSome_le c) + · intro q ⟨c, b⟩ _ p hp _ + cases q with + | forward x => + dsimp [forgetfulWithBad] at hp + cases hx : c.lookup x with + | some y => + rw [hx, PMF.mem_support_pure_iff] at hp + rw [hp] + exact Nat.le_succ _ + | none => + rw [hx, PMF.mem_support_map_iff] at hp + obtain ⟨y₀, -, rfl⟩ := hp + simp + | inverse y => + dsimp [forgetfulWithBad] at hp + cases hy : invLookup c y with + | some x => + rw [hy, PMF.mem_support_pure_iff] at hp + rw [hp] + exact Nat.le_succ _ + | none => + rw [hy, PMF.mem_support_map_iff] at hp + obtain ⟨x₀, -, rfl⟩ := hp + simp + +/-- **Bidirectional random-permutation switching inequality (`ℝ≥0∞`, one-sided)**: for any +`Q`-query adaptive program, evaluating against a uniform permutation accepts within +`Q.choose 2 * |α|⁻¹` of evaluating against `forgetfulAnswer`. -/ +theorem uniformPerm_bind_apply_le_forgetful {β γ : Type} + {program : OracleComp (PermOracleSpec α) β} {Q : ℕ} + (hQ : IsQueryBounded program Q) (next : β → PMF γ) (c : γ) : + ((do + let π ← PMF.uniformOfFintype (Equiv.Perm α) + OracleComp.interpret (fun q => PMF.pure (evalPerm π q)) program).bind next) c ≤ + ((((OracleComp.interpret forgetfulAnswer program).run []).map Prod.fst).bind next) c + + (Q.choose 2 : ℝ≥0∞) * (Fintype.card α : ℝ≥0∞)⁻¹ := by + rw [uniform_interpret_eq_lazy, + ← run_interpret_exactWithBad_map_fst program [] false isPartialBijection_nil, + ← run_interpret_forgetfulWithBad_map_fst program [] false] + simp only [PMF.map_comp, Function.comp_def, PMF.bind_map] + have hdiff := identicalUntilBad_exactWithBad_forgetfulWithBad.bind_apply_le + program ([], false) (fun x => next x.1) c + rw [identicalUntilBad_exactWithBad_forgetfulWithBad.bad_eq] at hdiff + refine hdiff.trans (add_le_add le_rfl ?_) + have hbad := toOuterMeasure_bad_forgetfulWithBad_le hQ [] + simpa only [List.length_nil, mul_zero, zero_add] using hbad + +/-- **Bidirectional random-permutation switching bound (`ℝ`, two-sided, [BonehShoup2023], +Section 4.7)**: for any `Q`-query adaptive program, the output distributions under a uniform +permutation `π ← PMF.uniformOfFintype (Equiv.Perm α)` and under the forgetful lazy sampler +`forgetfulAnswer` differ in probability on every event by at most `Q.choose 2 / |α|`. -/ +theorem abs_sub_uniformPerm_forgetful_le {β γ : Type} + {program : OracleComp (PermOracleSpec α) β} {Q : ℕ} + (hQ : IsQueryBounded program Q) (next : β → PMF γ) (c : γ) : + |(((do + let π ← PMF.uniformOfFintype (Equiv.Perm α) + OracleComp.interpret (fun q => PMF.pure (evalPerm π q)) program).bind next) c).toReal - + (((((OracleComp.interpret forgetfulAnswer program).run []).map + Prod.fst).bind next) c).toReal| ≤ + (Q.choose 2 : ℝ) * (Fintype.card α : ℝ)⁻¹ := by + rw [uniform_interpret_eq_lazy, + ← run_interpret_exactWithBad_map_fst program [] false isPartialBijection_nil, + ← run_interpret_forgetfulWithBad_map_fst program [] false] + simp only [PMF.map_comp, Function.comp_def, PMF.bind_map] + have hdiff := identicalUntilBad_exactWithBad_forgetfulWithBad.abs_sub_le + program ([], false) (fun x => next x.1) c + rw [identicalUntilBad_exactWithBad_forgetfulWithBad.bad_eq] at hdiff + refine hdiff.trans ?_ + have hbad := toOuterMeasure_bad_forgetfulWithBad_le hQ [] + simp only [List.length_nil, mul_zero, zero_add] at hbad + have htop : ((Q.choose 2 : ℕ) : ℝ≥0∞) * (Fintype.card α : ℝ≥0∞)⁻¹ ≠ ⊤ := + ENNReal.mul_ne_top (ENNReal.natCast_ne_top _) + (ENNReal.inv_ne_top.mpr (Nat.cast_ne_zero.mpr Fintype.card_ne_zero)) + simpa only [ENNReal.toReal_mul, ENNReal.toReal_natCast, ENNReal.toReal_inv] using + ENNReal.toReal_mono htop hbad + +/-- **The PRP/PRF switching lemma (`ℝ`, two-sided, [BonehShoup2023], Section 4.4, Theorem 4.4)**: +for any `Q`-query forward-only adaptive program `program : OracleComp (fun _ : α => α) β`, the +acceptance probabilities under a uniformly random permutation +`π ← PMF.uniformOfFintype (Equiv.Perm α)` and under a uniformly random function +`f ← PMF.uniformOfFintype (α → α)` differ by at most `Q.choose 2 / |α|`. -/ +theorem abs_sub_uniformPerm_uniformFunc_le {β γ : Type} + {program : OracleComp (fun _ : α => α) β} {Q : ℕ} + (hQ : IsQueryBounded program Q) (next : β → PMF γ) (c : γ) : + |(((do + let π ← PMF.uniformOfFintype (Equiv.Perm α) + OracleComp.interpret (fun x => PMF.pure (π x)) program).bind next) c).toReal - + (((do + let f ← PMF.uniformOfFintype (α → α) + OracleComp.interpret (fun x => PMF.pure (f x)) program).bind next) c).toReal| ≤ + (Q.choose 2 : ℝ) * (Fintype.card α : ℝ)⁻¹ := by + have h := abs_sub_uniformPerm_forgetful_le (isQueryBounded_liftForward hQ) next c + have hperm : + (do + let π ← PMF.uniformOfFintype (Equiv.Perm α) + OracleComp.interpret (fun q => PMF.pure (evalPerm π q)) (liftForward program)) = + (do + let π ← PMF.uniformOfFintype (Equiv.Perm α) + OracleComp.interpret (fun x => PMF.pure (π x)) program) := by + simp only [interpret_evalPerm_liftForward] + have hfunc : + (((OracleComp.interpret forgetfulAnswer (liftForward program)).run []).map Prod.fst) = + (do + let f ← PMF.uniformOfFintype (α → α) + OracleComp.interpret (fun x => PMF.pure (f x)) program) := by + rw [run_interpret_forgetfulAnswer_liftForward] + have hm := RandomOracle.interpret_eq_memoize + (fun _ : α => PMF.uniformOfFintype α) program + rw [Probability.PMF.pi_uniformOfFintype] at hm + exact hm.symm + rwa [hperm, hfunc] at h + +end Finite + +end Cslib.RandomPermutation diff --git a/ComplexityTests/Crypto/EvenMansour.lean b/ComplexityTests/Crypto/EvenMansour.lean index 964d8ddb90..0f6397495f 100644 --- a/ComplexityTests/Crypto/EvenMansour.lean +++ b/ComplexityTests/Crypto/EvenMansour.lean @@ -85,6 +85,11 @@ example (T_e T_π : List (BitString 4 × BitString 4)) : 2 * (T_e.length : ℝ) * (T_π.length : ℝ) / (Fintype.card (BitString 4) : ℝ) := toOuterMeasure_isBadSingleKeyEvenMansour_toReal_le T_e T_π +example (program : OracleComp (EvenMansourSpec (BitString 4)) Bool) : + evenMansourIdealGame program = + (((OracleComp.interpret idealLazyHandler program).run ([], [])).map Prod.fst : PMF Bool) := + evenMansourIdealGame_eq_lazy program + /-! ### Axiom guards for headline results -/ /-- @@ -184,4 +189,11 @@ info: 'Cslib.Crypto.EvenMansour.IsCallBounded.badSingleKeyEvenMansour_toReal_le' #guard_msgs in #print axioms IsCallBounded.badSingleKeyEvenMansour_toReal_le +/-- +info: 'Cslib.Crypto.EvenMansour.evenMansourIdealGame_eq_lazy' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms evenMansourIdealGame_eq_lazy + end Cslib.Crypto.EvenMansour.Tests diff --git a/ComplexityTests/Crypto/LubyRackoff.lean b/ComplexityTests/Crypto/LubyRackoff.lean index 65a85ccc6d..77fd42ff9a 100644 --- a/ComplexityTests/Crypto/LubyRackoff.lean +++ b/ComplexityTests/Crypto/LubyRackoff.lean @@ -116,6 +116,32 @@ example (keyGen : PMF (ZMod 7)) (F : ZMod 7 → ZMod 7 → ZMod 7) {ε₁ ε₂ ε₁ + ε₂ + ε₃ + 2 * ((2 : ℕ).choose 2 : ℝ) * (Fintype.card (ZMod 7) : ℝ)⁻¹ := advantage_feistel3KeyedGame_randomFunctionGame_le isQueryBounded_sampleDistinguisher h₁ h₂ h₃ +-- Concrete instantiation of the 3-round Luby–Rackoff PRP bound against a uniform random +-- permutation (`idealPermGame`) over `ZMod 7 × ZMod 7`. +example : + (Game.advantage (feistel3RandomRoundsGame sampleDistinguisher) + (idealPermGame sampleDistinguisher) : ℝ) ≤ + 2 * ((2 : ℕ).choose 2 : ℝ) * (Fintype.card (ZMod 7) : ℝ)⁻¹ + + ((2 : ℕ).choose 2 : ℝ) * ((Fintype.card (ZMod 7) : ℝ)⁻¹) ^ 2 := + advantage_feistel3RandomRoundsGame_idealPermGame_le isQueryBounded_sampleDistinguisher + +-- Concrete instantiation of the full keyed 3-round Luby–Rackoff PRP theorem over `ZMod 7`. +example (keyGen : PMF (ZMod 7)) (F : ZMod 7 → ZMod 7 → ZMod 7) {ε₁ ε₂ ε₃ : ℝ} + (h₁ : ∀ g₂ g₃, + (Game.advantage (prfSingleRealGame keyGen F (feistel3Reduction₁ g₂ g₃ sampleDistinguisher)) + (prfSingleIdealGame (feistel3Reduction₁ g₂ g₃ sampleDistinguisher)) : ℝ) ≤ ε₁) + (h₂ : ∀ g₁ g₃, + (Game.advantage (prfSingleRealGame keyGen F (feistel3Reduction₂ g₁ g₃ sampleDistinguisher)) + (prfSingleIdealGame (feistel3Reduction₂ g₁ g₃ sampleDistinguisher)) : ℝ) ≤ ε₂) + (h₃ : ∀ g₁ g₂, + (Game.advantage (prfSingleRealGame keyGen F (feistel3Reduction₃ g₁ g₂ sampleDistinguisher)) + (prfSingleIdealGame (feistel3Reduction₃ g₁ g₂ sampleDistinguisher)) : ℝ) ≤ ε₃) : + (Game.advantage (feistel3KeyedGame keyGen F sampleDistinguisher) + (idealPermGame sampleDistinguisher) : ℝ) ≤ + ε₁ + ε₂ + ε₃ + 2 * ((2 : ℕ).choose 2 : ℝ) * (Fintype.card (ZMod 7) : ℝ)⁻¹ + + ((2 : ℕ).choose 2 : ℝ) * ((Fintype.card (ZMod 7) : ℝ)⁻¹) ^ 2 := + advantage_feistel3KeyedGame_idealPermGame_le isQueryBounded_sampleDistinguisher h₁ h₂ h₃ + -- Concrete instantiation of the bit-string specialization on `BitString 4`. example (D : OracleComp (fun _ : BitString 4 × BitString 4 => BitString 4 × BitString 4) Bool) (hQ : OracleComp.IsQueryBounded D 2) : @@ -161,6 +187,36 @@ example : advantage_feistel3CCAAttack_idealStrongGame_pos f₁ f₂ f₃ (l₂ := (2 : ZMod 7)) (by decide) (by decide) (by decide) +-- Quantitative nonnegligible lower bound `1 - 1 / |G| - 4 / |G|²` against `idealStrongGame` +-- over `ZMod 7` (`l₀ = 0 ≠ 1 = l₁, r₀ = 2`, giving advantage at least `38 / 49`). +example : + 1 - (Fintype.card (ZMod 7) : ℝ)⁻¹ - 4 * ((Fintype.card (ZMod 7) : ℝ)⁻¹) ^ 2 ≤ + (Game.advantage + (OracleComp.interpret (feistelStrongOracle (feistel3 f₁ f₂ f₃)) + (feistel3CCAAttack (0 : ZMod 7) 1 2)) + (idealStrongGame (feistel3CCAAttack (0 : ZMod 7) 1 2)) : ℝ) := + le_advantage_feistel3CCAAttack_idealStrongGame_of_ne f₁ f₂ f₃ (by decide) + +-- Concrete `Fin 3` instance for `RandomPermutation.uniform_interpret_eq_lazy` and +-- `RandomPermutation.abs_sub_uniformPerm_forgetful_le`. +example (program : OracleComp (RandomPermutation.PermOracleSpec (Fin 3)) Bool) : + (do + let π ← PMF.uniformOfFintype (Equiv.Perm (Fin 3)) + OracleComp.interpret (fun q => PMF.pure (RandomPermutation.evalPerm π q)) program) = + (((OracleComp.interpret RandomPermutation.answer program).run []).map Prod.fst) := + RandomPermutation.uniform_interpret_eq_lazy program + +example (program : OracleComp (RandomPermutation.PermOracleSpec (Fin 3)) Bool) + (hQ : OracleComp.IsQueryBounded program 2) : + |(((do + let π ← PMF.uniformOfFintype (Equiv.Perm (Fin 3)) + OracleComp.interpret (fun q => PMF.pure (RandomPermutation.evalPerm π q)) program).bind + PMF.pure) true).toReal - + (((((OracleComp.interpret RandomPermutation.forgetfulAnswer program).run []).map + Prod.fst).bind PMF.pure) true).toReal| ≤ + ((2 : ℕ).choose 2 : ℝ) * (Fintype.card (Fin 3) : ℝ)⁻¹ := + RandomPermutation.abs_sub_uniformPerm_forgetful_le hQ PMF.pure true + -- Separation against the independent-table game `independentTableStrongGame` over `ZMod 7`. example : independentTableStrongGame (feistel3CCAAttack (0 : ZMod 7) 1 2) true = @@ -313,4 +369,81 @@ depends on axioms: [propext, Classical.choice, Quot.sound] #print axioms Cslib.Crypto.LubyRackoff.advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le +/-- +info: 'Cslib.RandomPermutation.answer_complete' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.RandomPermutation.answer_complete + +/-- +info: 'Cslib.RandomPermutation.uniform_interpret_eq_lazy' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.RandomPermutation.uniform_interpret_eq_lazy + +/-- +info: 'Cslib.RandomPermutation.uniformPerm_bind_apply_le_forgetful' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.RandomPermutation.uniformPerm_bind_apply_le_forgetful + +/-- +info: 'Cslib.RandomPermutation.abs_sub_uniformPerm_forgetful_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.RandomPermutation.abs_sub_uniformPerm_forgetful_le + +/-- +info: 'Cslib.RandomPermutation.abs_sub_uniformPerm_uniformFunc_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.RandomPermutation.abs_sub_uniformPerm_uniformFunc_le + +/-- +info: 'Cslib.RandomPermutation.toOuterMeasure_bad_choose_two_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.RandomPermutation.toOuterMeasure_bad_choose_two_le + +/-- +info: 'Cslib.Crypto.LubyRackoff.advantage_idealPermGame_randomFunctionGame_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.LubyRackoff.advantage_idealPermGame_randomFunctionGame_le + +/-- +info: 'Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_idealPermGame_le' depends on +axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.LubyRackoff.advantage_feistel3RandomRoundsGame_idealPermGame_le + +/-- +info: 'Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_idealPermGame_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.LubyRackoff.advantage_feistel3KeyedGame_idealPermGame_le + +/-- +info: 'Cslib.Crypto.LubyRackoff.idealStrongGame_feistel3CCAAttack_true_le' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.LubyRackoff.idealStrongGame_feistel3CCAAttack_true_le + +/-- +info: 'Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame_of_ne' depends on +axioms: [propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms Cslib.Crypto.LubyRackoff.le_advantage_feistel3CCAAttack_idealStrongGame_of_ne + end ComplexityTests.Crypto.LubyRackoff diff --git a/ROADMAP.md b/ROADMAP.md index 3ef44e9c74..dcbcea0bd0 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1186,21 +1186,28 @@ Jukna coverage below is an additional target beyond the V1 port: [Carter–Wegman polynomial](Complexity/Probability/HashFamily/Polynomial.lean) and [multiply-shift](Complexity/Probability/HashFamily/MultiplyShift.lean) families are proved. [Feistel networks and the Luby–Rackoff theorem](Complexity/Crypto/Protocols/Cipher/LubyRackoff.lean) - (#748, Boneh–Shoup Section 4.4 / Luby–Rackoff 1988) prove the `Q.choose 2 * ε + Q.choose 2 / |G|` + (#748, #834, Boneh–Shoup Section 4.4 / Luby–Rackoff 1988), backed by the shared + [lazy bidirectional random-permutation sampler](Complexity/Languages/Probabilistic/RandomPermutation.lean) + (#834), prove the `Q.choose 2 * ε + Q.choose 2 / |G|` 3-round adaptive CPA bound with Δ-universal Round 1 (`advantage_feistel3HashIdealGame_randomFunctionGame_le`), the `2 * Q.choose 2 / |G|` uniform-random-round corollary (`advantage_feistel3RandomRoundsGame_randomFunctionGame_le`), the 3-round and 4-round PRF-to-Feistel hybrid bounds (`advantage_feistel3KeyedGame_randomFunctionGame_le`, - `advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le`), and the 3-query + `advantage_feistel4StrongKeyedGame_feistel4StrongRandomRoundsGame_le`), the PRP-PRF switching + bound `Q.choose 2 / |G|²` and 3-round PRP bounds against a uniform random permutation + (`advantage_idealPermGame_randomFunctionGame_le`, + `advantage_feistel3RandomRoundsGame_idealPermGame_le`, + `advantage_feistel3KeyedGame_idealPermGame_le`), and the 3-query chosen-ciphertext attack against 3-round Feistel (`eval_feistel3_feistel3CCAAttack`, with the equal-input sanity check `advantage_feistel3CCAAttack_self`, the finite positive gap `(|Equiv.Perm (G × G)|)⁻¹ ≤ advantage` against the true bidirectional random-permutation game - `idealStrongGame` for `|G| ≥ 3` in `le_advantage_feistel3CCAAttack_idealStrongGame`, and the - separate exact `1 - |G|⁻¹` bound against the independent-table benchmark - `independentTableStrongGame` in `advantage_feistel3CCAAttack_independentTable`). Open in #748: a - quantitative nonnegligible CCA advantage lower bound against `idealStrongGame` as the block size - grows, and the 4-round information-theoretic bidirectional random-round collision bound. + `idealStrongGame` for `|G| ≥ 3` in `le_advantage_feistel3CCAAttack_idealStrongGame`, the + quantitative nonnegligible lower bound `1 - |G|⁻¹ - 4 / |G|² ≤ advantage` against + `idealStrongGame` for any `l₀ ≠ l₁` in `le_advantage_feistel3CCAAttack_idealStrongGame_of_ne`, + and the separate exact `1 - |G|⁻¹` bound against the independent-table benchmark + `independentTableStrongGame` in `advantage_feistel3CCAAttack_independentTable`). Open in #748: + the 4-round information-theoretic bidirectional random-round collision bound. Open: the leftover hash lemma stated over `ε`-universal families, with `IsTwoUniversal` as its `1 / |Y|` case and the pseudoentropy clients updated. * **Sigma protocols, Schnorr identification and Fiat–Shamir (#581).** Boneh–Shoup Chapter 19. @@ -1274,13 +1281,15 @@ Jukna coverage below is an additional target beyond the V1 port: (#736, including one-time, adaptive multi-query issued-counter, arbitrary-pad hybrid, and exact single-query fixed-nonce `prfRealGame`/`prfIdealGame` reduction bounds), and the Even–Mansour cipher in the ideal-permutation model (algebraic permutations, one-query secrecy, one-sided query - security, 2-query breaks when omitting either whitening key, and the Boneh–Shoup Theorem 4.10 - bad-key transcript intersection bound `2 * Q_e * Q_π / |G|`, #761). + security, 2-query breaks when omitting either whitening key, the Boneh–Shoup Theorem 4.10 + bad-key transcript intersection bound `2 * Q_e * Q_π / |G|`, and exact equivalence of the + two-sided ideal game with two independent lazy bidirectional random-permutation samplers in + `evenMansourIdealGame_eq_lazy`, #761, #834). Open: `IsOraclePPT` admissibility, uniform word-level forger/hash families, the asymptotic `PseudorandomFunction` corollary, and fresh-nonce multi-query Carter–Wegman MAC security; - lazy-sampled bidirectional random-permutation coupling connecting the Even–Mansour bad-key - intersection bound to full two-sided `Game.advantage`; Luby–Rackoff (three Feistel rounds over a - PRF give a PRP, four give a strong PRP); and the Naor–Reingold PRF from the decisional + coupling the Even–Mansour real game with the lazy ideal game via the bad-key transcript + intersection bound to bound full two-sided `Game.advantage`; the 4-round strong Feistel + information-theoretic collision bound (#748); and the Naor–Reingold PRF from the decisional Diffie–Hellman assumption. * **Lattice Sigma protocols and post-quantum signatures (#640, track B).** Proved (#645): the