diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index 42e1b77cd4..5da5039116 100644 --- a/Complexity/Crypto/Computational/Nonuniform/Basic.lean +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -27,8 +27,10 @@ family need not be computable, so it can hard-wire information about every param `NonuniformlyIndistinguishable`, `NonuniformOneWay` and `NonuniformPRG` relativize `ComputationallyIndistinguishable`, `OneWay` and `PseudorandomGenerator` to this class. Each uniform adversary is an advice adversary that ignores empty advice, so every nonuniform notion -implies its uniform counterpart. Moreover, an advice word may carry a value of any type under -any encoding (`NonuniformlyIndistinguishable.negligible_encoded`, +implies its uniform counterpart. `IndistinguishableWithAdvice advice` fixes one advice family; +with empty advice it is exactly uniform indistinguishability, so a reduction proved relative to a +fixed family yields both the uniform and the nonuniform theorem. Moreover, an advice word may carry +a value of any type under any encoding (`IndistinguishableWithAdvice.negligible_encoded`, `NonuniformOneWay.inversion_negligible_encoded`): an adversary need not decode its advice, since it may run on the encoded word exactly as on the typed value. @@ -36,8 +38,10 @@ These are definitions, not assertions that such primitives exist. ## Main definitions -* `Cslib.Crypto.NonuniformlyIndistinguishable`: indistinguishability against uniform strict PPT - tests given polynomially bounded advice. +* `Cslib.Crypto.IndistinguishableWithAdvice`: indistinguishability against uniform strict PPT + tests given one fixed advice family. +* `Cslib.Crypto.NonuniformlyIndistinguishable`: indistinguishability with every polynomially + bounded advice family. * `Cslib.Crypto.NonuniformOneWay`: one-wayness against inverters given polynomially bounded advice. * `Cslib.Crypto.NonuniformPRG`: a stretching generator whose output is nonuniformly @@ -52,7 +56,10 @@ These are definitions, not assertions that such primitives exist. * `Cslib.Crypto.NonuniformlyIndistinguishable.computationallyIndistinguishable`, `Cslib.Crypto.NonuniformOneWay.toOneWay`, `Cslib.Crypto.NonuniformPRG.toPRG`: nonuniform security implies uniform security. -* `Cslib.Crypto.NonuniformlyIndistinguishable.negligible_encoded`, +* `Cslib.Crypto.computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil`: uniform + indistinguishability is indistinguishability with empty advice. +* `Cslib.Crypto.IndistinguishableWithAdvice.map`: efficient postprocessing. +* `Cslib.Crypto.IndistinguishableWithAdvice.negligible_encoded`, `Cslib.Crypto.NonuniformOneWay.inversion_negligible_encoded`: advice of any encoded type. * `Cslib.Crypto.not_computationallyIndistinguishable_pure_uniformList`, `Cslib.Crypto.not_nonuniformlyIndistinguishable_pure_uniformList`: fixed words are @@ -78,18 +85,59 @@ private theorem isPPTOn_dropAdvice {β : Type} {output : β ↪ List Bool} h.on.preprocess (input := encPair (encPair encUnary encBits) encBits) (prepare := fun input : (ℕ × List Bool) × List Bool => (input.1.1, input.2)) (by fun_prop) -/-- Two ensembles are **nonuniformly indistinguishable** when, for every polynomially bounded -advice family, each uniform strict PPT test reading the parameter, the advice word and a sample -has negligible advantage. The test's clock is polynomial in the length of its whole input, -including the sample, as for `ComputationallyIndistinguishable`: for ensembles of superpolynomial -sample length the test gets more than `poly(n)` time, unlike a polynomial-size circuit. -/ +/-- Two ensembles are **indistinguishable with advice** `advice` when each uniform strict PPT +test reading the parameter `n`, the advice word `advice n` and a sample has negligible advantage. +The advice family is not bounded here; its length is charged to the test's clock, which is +polynomial in the length of its whole input, including the advice and the sample, as for +`ComputationallyIndistinguishable`: for ensembles of superpolynomial sample length the test gets +more than `poly(n)` time, unlike a polynomial-size circuit. With empty advice this is uniform +computational indistinguishability +(`computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil`). -/ +def IndistinguishableWithAdvice (advice : ℕ → List Bool) (X Y : ℕ → PMF (List Bool)) : Prop := + Game.Indistinguishable + (fun (test : (ℕ × List Bool) × List Bool → ProbComp Bool) n => + distinguishingGame (X n) (fun word => test ((n, advice n), word))) + (fun test n => distinguishingGame (Y n) (fun word => test ((n, advice n), word))) + (IsPPTOn (encPair (encPair encUnary encBits) encBits) encBool) + +/-- Two ensembles are **nonuniformly indistinguishable** when they are indistinguishable with +every polynomially bounded advice family. -/ def NonuniformlyIndistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → - Game.Indistinguishable - (fun (test : (ℕ × List Bool) × List Bool → ProbComp Bool) n => - distinguishingGame (X n) (fun word => test ((n, advice n), word))) - (fun test n => distinguishingGame (Y n) (fun word => test ((n, advice n), word))) - (IsPPTOn (encPair (encPair encUnary encBits) encBits) encBool) + IndistinguishableWithAdvice advice X Y + +/-- **Uniform indistinguishability is the empty-advice case.** A uniform test is an advice test +that ignores its advice, and an advice test run on empty advice is a uniform test. -/ +theorem computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil + {X Y : ℕ → PMF (List Bool)} : + ComputationallyIndistinguishable X Y ↔ IndistinguishableWithAdvice (fun _ => []) X Y := by + constructor + · intro h test htest + have hprepare : ComputableInPolyTime (fun input : ℕ × List Bool => ((input.1, []), input.2)) + (encPair encUnary encBits) (encPair (encPair encUnary encBits) encBits) := by fun_prop + exact h (fun n word => test ((n, []), word)) (htest.preprocess hprepare) + · intro h adversary hadversary + have hneg := h (fun input => adversary input.1.1 input.2) (isPPTOn_dropAdvice hadversary) + simpa only using hneg + +/-- Efficient parameter-dependent deterministic postprocessing preserves indistinguishability +with advice. -/ +theorem IndistinguishableWithAdvice.map {advice : ℕ → List Bool} {X Y : ℕ → PMF (List Bool)} + (h : IndistinguishableWithAdvice advice X Y) {f : ℕ → List Bool → List Bool} + (hf : ComputableInPolyTime (fun (n, word) => f n word) (encPair encUnary encBits) encBits) : + IndistinguishableWithAdvice advice (fun n => (X n).map (f n)) (fun n => (Y n).map (f n)) := by + intro test htest + have hprepare : ComputableInPolyTime + (fun input : (ℕ × List Bool) × List Bool => (input.1, f input.1.1 input.2)) + (encPair (encPair encUnary encBits) encBits) + (encPair (encPair encUnary encBits) encBits) := by + have hpair : ComputableInPolyTime (fun input : (ℕ × List Bool) × List Bool => + (input.1.1, input.2)) (encPair (encPair encUnary encBits) encBits) + (encPair encUnary encBits) := by fun_prop + exact (ComputableInPolyTime.fst _ _).prod (hf.comp hpair) + have hneg := h (fun input => test (input.1, f input.1.1 input.2)) (htest.preprocess hprepare) + simpa only [distinguishingGame, PMF.monad_bind_eq_bind, PMF.bind_map, Function.comp_def] + using hneg /-- Every ensemble is nonuniformly indistinguishable from itself. -/ theorem NonuniformlyIndistinguishable.refl (X : ℕ → PMF (List Bool)) : @@ -110,21 +158,20 @@ theorem NonuniformlyIndistinguishable.trans {X Y Z : ℕ → PMF (List Bool)} empty advice. -/ theorem NonuniformlyIndistinguishable.computationallyIndistinguishable {X Y : ℕ → PMF (List Bool)} (h : NonuniformlyIndistinguishable X Y) : - ComputationallyIndistinguishable X Y := by - intro adversary hadversary - have hneg := h (fun _ => []) (PolynomiallyBounded.const 0) - (fun input => adversary input.1.1 input.2) (isPPTOn_dropAdvice hadversary) - simpa only using hneg - -/-- **Advice of any encoded type.** Under nonuniform indistinguishability, a uniform strict PPT -test may read an advice value of an arbitrary type `γ`, under an arbitrary encoding with -polynomially bounded lengths. The test need not be able to decode the advice word: the proof runs -its machine on that word (`Cslib.Probability.IsPPTOn.exists_extension`). -/ -theorem NonuniformlyIndistinguishable.negligible_encoded {X Y : ℕ → PMF (List Bool)} - (h : NonuniformlyIndistinguishable X Y) {γ : Type} {encAdvice : γ ↪ List Bool} + ComputationallyIndistinguishable X Y := + computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil.mpr + (h _ (PolynomiallyBounded.const 0)) + +/-- **Advice of any encoded type.** Indistinguishability with the advice words +`encAdvice (advice n)` covers every uniform strict PPT test that reads the advice value +`advice n` itself, of an arbitrary type `γ` under an arbitrary encoding. The test need not be able +to decode the advice word: the proof runs its machine on that word +(`Cslib.Probability.IsPPTOn.exists_extension`). -/ +theorem IndistinguishableWithAdvice.negligible_encoded {X Y : ℕ → PMF (List Bool)} + {γ : Type} {encAdvice : γ ↪ List Bool} {advice : ℕ → γ} + (h : IndistinguishableWithAdvice (fun n => encAdvice (advice n)) X Y) {test : (ℕ × γ) × List Bool → ProbComp Bool} - (htest : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBool test) - {advice : ℕ → γ} (hadvice : PolynomiallyBounded (fun n => (encAdvice (advice n)).length)) : + (htest : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBool test) : Negligible (fun n => Game.advantage (distinguishingGame (X n) (fun word => test ((n, advice n), word))) (distinguishingGame (Y n) (fun word => test ((n, advice n), word)))) := by @@ -137,8 +184,7 @@ theorem NonuniformlyIndistinguishable.negligible_encoded {X Y : ℕ → PMF (Lis ProbComp.eval (extension (encPair (encPair encUnary encBits) encBits ((n, encAdvice (advice n)), word))) = ProbComp.eval (test ((n, advice n), word)) := heq ((n, advice n), word) - simpa only [distinguishingGame, hkey] using - h (fun n => encAdvice (advice n)) hadvice _ hword + simpa only [distinguishingGame, hkey] using h _ hword /-- **Fixed words are distinguishable from uniform words**, already by a uniform test: the first bit of `PMF.pure (target n)` is constant, while that of a uniform word of positive length is a fair diff --git a/Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean b/Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean index 2475a0e152..3c3608a042 100644 --- a/Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean +++ b/Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean @@ -66,7 +66,7 @@ theorem NonuniformPRG.advicePRG {generator : List Bool → List Bool} {length : (encAdvice (a (m - 7), w (m - 7), z (m - 7))).length) := by simp only [encAdvice, length_encPair, encBits, Function.Embedding.coe_refl, id] fun_prop - have hneg := (h.secure.negligible_encoded hshift hadvice).shift 7 + have hneg := ((h.secure _ hadvice).negligible_encoded hshift).shift 7 refine hneg.congr' (Filter.Eventually.of_forall fun n => ?_) simp only [Nat.add_sub_cancel, eval_bind_eq_distinguishingGame, ProbComp.eval_map, BitString.eval_sampleList, generatorEnsemble] diff --git a/Complexity/Crypto/Computational/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean index acb98160fe..5ad48945d5 100644 --- a/Complexity/Crypto/Computational/Stretch.lean +++ b/Complexity/Crypto/Computational/Stretch.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Crypto.Computational.Nonuniform.Basic public import Complexity.Crypto.Computational.PseudorandomGenerator public import Complexity.Crypto.Computational.Stretch.Quantitative public import Complexity.Languages.Probabilistic.UniformNat @@ -23,8 +24,10 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Pl Keep a seed of the original length at the front of a word. Each iteration expands that seed by one bit and retains the previously emitted suffix. The security proof replaces successive seed expansions by uniform bits, using one uniformly randomized reduction across all hops. -The seed width may differ from the security parameter, and the generator may capture an index. -`indexed_indistinguishable` preserves a secure choice in such a family. +The seed width may differ from the security parameter, and the generator may capture a context. +`indexed_indistinguishable` preserves a secure choice in such a family. Taking the context to be +an advice word gives the stretch theorem relative to fixed advice, from which both the uniform and +the nonuniform (advice-secure) versions follow. The deterministic iteration and stretch operators (`PRGStretch.step`, `PRGStretch.iterate`, `PRGStretch.stretch`) and their polynomial-time and cumulative quantitative certificates live in @@ -41,10 +44,14 @@ The deterministic iteration and stretch operators (`PRGStretch.step`, `PRGStretc * `PRGStretch.polyTime_iterate`: captured functional iteration has a uniform TM certificate (re-exported from `Stretch.Quantitative`). * `PRGStretch.advantage_eq`: exact sampling-range loss for the uniform reduction. -* `PRGStretch.indexed_indistinguishable`, `PRGStretch.indistinguishable`, - `PRGStretch.pseudorandomGenerator`: polynomially many one-bit expansions preserve computational - indistinguishability and yield a secure PRG. -* `PseudorandomGenerator.amplify`, `.truncate`: efficient changes of output length. +* `PRGStretch.indexed_indistinguishable`: polynomially many one-bit expansions preserve the + security of a chosen member of a family, for a chosen context of any encoded type. +* `PRGStretch.indistinguishableWithAdvice`: the same for one generator, relative to a fixed advice + family; `PRGStretch.indistinguishable` is its empty-advice case. +* `PRGStretch.pseudorandomGenerator`, `PRGStretch.nonuniformPRG`: polynomial stretch of uniform and + nonuniform one-bit PRGs. +* `PseudorandomGenerator.amplify`, `.truncate`, `NonuniformPRG.amplify`, `.truncate`: efficient + changes of output length. ## References @@ -183,26 +190,6 @@ theorem isPPT_test {α : Type} {input : α ↪ List Bool} simpa only [test, reduction, hop, pairEncoding, fullEncoding, Function.comp_def] using hindex.bind_with hbranch -/-- The reduction's complete efficiency proof uses the public programming interface. -/ -@[program_certificate] -theorem isPPT_reduction {generator : List Bool → List Bool} {count : ℕ → ℕ} - {adversary : Distinguisher} (hgenerator : ComputableInPolyTime generator encBits encBits) - (hcount : ComputableInPolyTime count encUnary encUnary) - (hadversary : IsPPT encBool adversary) : - IsPPT encBool (reduction generator count adversary) := by - have hgen : ComputableInPolyTime - (fun p : (ℕ × List Bool) × List Bool => generator p.2) - (encPair (encPair encUnary encBits) encBits) encBits := - hgenerator.comp (ComputableInPolyTime.snd (encPair encUnary encBits) encBits) - have hadv : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBool - (fun p => adversary p.1.1 p.2) := hadversary.on.preprocess - ((ComputableInPolyTime.fst (encPair encUnary encBits) encBits).fst'.prod - (ComputableInPolyTime.snd (encPair encUnary encBits) encBits)) - simpa only [IsPPT, test, reduction, hop, Function.comp_def] using - (isPPT_test hgen (ComputableInPolyTime.fst encUnary encBits) - (hcount.comp (ComputableInPolyTime.fst encUnary encBits)) hadv - (ComputableInPolyTime.snd encUnary encBits)) - /-- Capping a sampled index only merges rejecting branches. -/ theorem hop_min (generator : List Bool → List Bool) (count : ℕ → ℕ) (adversary : Distinguisher) @@ -348,65 +335,87 @@ theorem loss_polynomial {count : ℕ → ℕ} exact dyadicSize_polynomiallyBounded.comp hcount.polynomiallyBounded /-- Polynomially many expansions preserve the secure choice in a uniformly efficient family. -The choice is supplied only in the proof; each reduction receives its index as ordinary input. -/ -theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → List Bool} - {seedBits count choose : ℕ → ℕ} +The choice `choose n` is a context of any encoded type: a candidate index, an advice word, or +both. It is supplied only in the proof; each reduction receives its context as ordinary input. -/ +theorem indexed_indistinguishable {κ : Type} {encContext : κ ↪ List Bool} + {generator : ℕ → κ → List Bool → List Bool} {seedBits count : ℕ → ℕ} {choose : ℕ → κ} (hgenerator : ComputableInPolyTime - (fun ((n, i), seed) => generator n i seed) - (encPair (encPair encUnary encUnary) encBits) encBits) + (fun ((n, context), seed) => generator n context seed) + (encPair (encPair encUnary encContext) encBits) encBits) (hseedBits : ComputableInPolyTime seedBits encUnary encUnary) (hcount : ComputableInPolyTime count encUnary encUnary) - (hsecure : ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, - IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun ((n, i), word) => adversary n i word) → + (hsecure : ∀ adversary : ℕ → κ → List Bool → ProbComp Bool, + IsPPTOn (encPair (encPair encUnary encContext) encBits) + encBool (fun ((n, context), word) => adversary n context word) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (generator n (choose n))).bind (fun word => ProbComp.eval (adversary n (choose n) word))) ((uniformList (seedBits n + 1)).bind (fun word => ProbComp.eval (adversary n (choose n) word))))) : - ∀ adversary : ℕ → ℕ → List Bool → ProbComp Bool, - IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun ((n, i), word) => adversary n i word) → + ∀ adversary : ℕ → κ → List Bool → ProbComp Bool, + IsPPTOn (encPair (encPair encUnary encContext) encBits) + encBool (fun ((n, context), word) => adversary n context word) → Negligible (fun n => Game.advantage (((uniformList (seedBits n)).map (iterate (generator n (choose n)) (seedBits n) (count n))).bind (fun word => ProbComp.eval (adversary n (choose n) word))) ((uniformList (seedBits n + count n)).bind (fun word => ProbComp.eval (adversary n (choose n) word)))) := by - simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] at hgenerator - simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] at hseedBits - simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] at hcount intro adversary hadversary - let reduction := fun n index => - test (generator n index) (seedBits n) (count n) (adversary n index) - have hprepare : ComputableTidilyInPolyTime - (fun p : ((ℕ × ℕ) × List Bool) × List Bool => (p.1.1, p.2)) - (encPair (encPair (encPair encUnary encUnary) encBits) encBits) - (encPair (encPair encUnary encUnary) encBits) := by fun_prop - have hreduce : IsPPTOn (encPair (encPair encUnary encUnary) encBits) - encBool (fun input => reduction input.1.1 input.1.2 input.2) := by + let reduction := fun n context => + test (generator n context) (seedBits n) (count n) (adversary n context) + have hprepare : ComputableInPolyTime + (fun p : ((ℕ × κ) × List Bool) × List Bool => (p.1.1, p.2)) + (encPair (encPair (encPair encUnary encContext) encBits) encBits) + (encPair (encPair encUnary encContext) encBits) := by fun_prop + have hparameter : ComputableInPolyTime (fun p : (ℕ × κ) × List Bool => p.1.1) + (encPair (encPair encUnary encContext) encBits) encUnary := by fun_prop + have hreduce : IsPPTOn (encPair (encPair encUnary encContext) encBits) + encBool (fun ((n, context), word) => reduction n context word) := by unfold reduction - exact isPPT_test (.of_tidy (hgenerator.comp hprepare)) (.of_tidy (by polytime)) - (.of_tidy (by polytime)) - (hadversary.preprocess (.of_tidy hprepare)) (.of_tidy (by polytime)) - have h := (hsecure reduction hreduce).polynomiallyBounded_mul (loss_polynomial (.of_tidy hcount)) + exact isPPT_test (hgenerator.comp hprepare) (hseedBits.comp hparameter) + (hcount.comp hparameter) (hadversary.preprocess hprepare) + (ComputableInPolyTime.snd _ _) + have h := (hsecure reduction hreduce).polynomiallyBounded_mul (loss_polynomial hcount) exact h.congr' (Filter.Eventually.of_forall (fun n => (test_advantage_eq _ _ _ _).symm)) +/-- **Polynomially many seed expansions, relative to fixed advice.** If a generator's output is +indistinguishable from uniform with the advice family `advice`, so is its efficient polynomial +stretch. Uniform security (`indistinguishable`) is the empty-advice case. -/ +theorem indistinguishableWithAdvice {generator : List Bool → List Bool} {count : ℕ → ℕ} + (hgenerator : ComputableInPolyTime generator encBits encBits) + (hcount : ComputableInPolyTime count encUnary encUnary) {advice : ℕ → List Bool} + (hsecure : IndistinguishableWithAdvice advice (generatorEnsemble generator) + (fun n => uniformList (n + 1))) : + IndistinguishableWithAdvice advice (generatorEnsemble (stretch generator count)) + (fun n => uniformList (n + count n)) := by + intro test htest + have hgen : ComputableInPolyTime + (fun (((_ : ℕ), (_ : List Bool)), seed) => generator seed) + (encPair (encPair encUnary encBits) encBits) encBits := + hgenerator.comp (ComputableInPolyTime.snd (encPair encUnary encBits) encBits) + have h := indexed_indistinguishable (generator := fun _ _ => generator) + (seedBits := fun n => n) (choose := advice) hgen + (ComputableInPolyTime.of_eq fun _ => rfl) hcount + (fun adversary hadversary => by + simpa only [distinguishingGame, generatorEnsemble, PMF.monad_bind_eq_bind] using + hsecure _ hadversary) + (fun n context word => test ((n, context), word)) htest + refine h.congr' (Filter.Eventually.of_forall fun n => ?_) + beta_reduce + rw [← hybrid_zero generator count n] + simp only [hybrid, distinguishingGame, PMF.monad_bind_eq_bind, Nat.add_zero, Nat.sub_zero] + /-- Polynomially many seed expansions preserve computational indistinguishability. -/ theorem indistinguishable {generator : List Bool → List Bool} {count : ℕ → ℕ} (hgenerator : PseudorandomGenerator generator (fun n => n + 1)) (hcount : ComputableInPolyTime count encUnary encUnary) : ComputationallyIndistinguishable (generatorEnsemble (stretch generator count)) - (fun n => uniformList (n + count n)) := by - have hcount := hcount.tidy - intro adversary hadversary - have hreduce := isPPT_reduction hgenerator.polyTime (.of_tidy hcount) hadversary - have hnegligible := hgenerator.indistinguishable _ hreduce - have hloss := hnegligible.polynomiallyBounded_mul (loss_polynomial (.of_tidy hcount)) - convert hloss using 1 - funext n - simpa only [eval_prgRealGame, eval_prgIdealGame] using - advantage_eq generator count adversary n + (fun n => uniformList (n + count n)) := + computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil.mpr + (indistinguishableWithAdvice hgenerator.polyTime hcount + (computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil.mp + hgenerator.indistinguishable)) /-- A positive efficiently computed number of one-bit expansions is a secure PRG. -/ theorem pseudorandomGenerator {generator : List Bool → List Bool} {count : ℕ → ℕ} @@ -423,6 +432,19 @@ theorem pseudorandomGenerator {generator : List Bool → List Bool} {count : ℕ · intro n exact Nat.lt_add_of_pos_right (hpositive n) +/-- A positive efficiently computed number of one-bit expansions of a nonuniform PRG is a +nonuniform PRG. -/ +theorem nonuniformPRG {generator : List Bool → List Bool} {count : ℕ → ℕ} + (hgenerator : NonuniformPRG generator (fun n => n + 1)) + (hcount : ComputableInPolyTime count encUnary encUnary) + (hpositive : ∀ n, 0 < count n) : + NonuniformPRG (stretch generator count) (fun n => n + count n) where + polyTime := polyTime_stretch hgenerator.polyTime hcount + length_eq _ := length_iterate hgenerator.length_eq _ _ _ + stretch n := Nat.lt_add_of_pos_right (hpositive n) + secure advice hadvice := + indistinguishableWithAdvice hgenerator.polyTime hcount (hgenerator.secure advice hadvice) + end Cslib.Crypto.PRGStretch namespace Cslib.Crypto @@ -462,4 +484,36 @@ theorem PseudorandomGenerator.truncate {generator : List Bool → List Bool} {le simpa only [← generatorEnsemble_postprocess generator (fun n word => word.take (target n)), uniformList_take (hle _)] using h +/-- Amplify a one-bit nonuniform PRG to any efficiently computed, strictly larger output +length. -/ +theorem NonuniformPRG.amplify {generator : List Bool → List Bool} + (hgenerator : NonuniformPRG generator (fun n => n + 1)) + (target : ℕ → ℕ) (htarget : ComputableInPolyTime target encUnary encUnary) + (hstretch : ∀ n, n < target n) : + NonuniformPRG (PRGStretch.stretch generator (fun n => target n - n)) target := by + have hcount : ComputableInPolyTime (fun n => target n - n) encUnary encUnary := by fun_prop + have h := PRGStretch.nonuniformPRG hgenerator hcount (fun n => by + have := hstretch n + lia) + convert h using 1 + funext n + have := hstretch n + lia + +/-- Truncating a nonuniform PRG to an efficiently computed, still-expanding length preserves +nonuniform security. -/ +theorem NonuniformPRG.truncate {generator : List Bool → List Bool} {length : ℕ → ℕ} + (hgenerator : NonuniformPRG generator length) + (target : ℕ → ℕ) + (htarget : ComputableInPolyTime target encUnary encUnary) + (hle : ∀ n, target n ≤ length n) (hstretch : ∀ n, n < target n) : + NonuniformPRG (fun seed => (generator seed).take (target seed.length)) target := by + have hpoly := hgenerator.polyTime + refine ⟨by fun_prop, fun seed => ?_, hstretch, fun advice hadvice => ?_⟩ + · simp only [List.length_take, hgenerator.length_eq, Nat.min_eq_left (hle _)] + · have h := (hgenerator.secure advice hadvice).map + (f := fun n word => word.take (target n)) (by fun_prop) + simpa only [← generatorEnsemble_postprocess generator (fun n word => word.take (target n)), + uniformList_take (hle _)] using h + end Cslib.Crypto diff --git a/ComplexityTests/Crypto/Nonuniform.lean b/ComplexityTests/Crypto/Nonuniform.lean index 9fb3cbd381..63ee3c5ed5 100644 --- a/ComplexityTests/Crypto/Nonuniform.lean +++ b/ComplexityTests/Crypto/Nonuniform.lean @@ -5,6 +5,7 @@ Authors: Samuel Schlesinger -/ import Complexity.Crypto.Computational.Nonuniform.ZeroKnowledge +import Complexity.Crypto.Computational.Stretch /-! Checked clients of the nonuniform security notions. Existence of a nonuniform one-way function or generator is open, so these checks show that the notions are not trivially true @@ -53,4 +54,19 @@ example {generator : List Bool → List Bool} {length : ℕ → ℕ} GMW.AdvicePRG Complexity.encCNF generator length := h.advicePRG _ +/-- With empty advice, indistinguishability with advice is uniform indistinguishability, so the +uniform first-bit separation transfers. -/ +example : ¬ IndistinguishableWithAdvice (fun _ => []) (fun n => PMF.pure (List.replicate n true)) + (fun n => BitString.uniformList n) := fun h => + not_computationallyIndistinguishable_pure_uniformList _ (Filter.eventually_ge_atTop 1) + (computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil.mpr h) + +/-- Stretching a nonuniform one-bit PRG to `3 * n + 1` bits, the GMW length, and feeding it to the +auxiliary-input GMW theorem. -/ +example {generator : List Bool → List Bool} (h : NonuniformPRG generator (fun n => n + 1)) + {α : Type} {enc : α ↪ List Bool} {A : Set α} (hA : A ∈ Complexity.NP enc) : + ∃ zk : ZeroKnowledgeProof enc A, zk.AuxiliaryInputZeroKnowledge := + (h.amplify (fun n => 3 * n + 1) (by fun_prop) (fun n => by omega)) + |>.exists_auxiliaryInputZeroKnowledge_of_mem_NP (fun _ => le_rfl) hA + end ComplexityTests.Crypto.Nonuniform