diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index 5da5039116..995515ac49 100644 --- a/Complexity/Crypto/Computational/Nonuniform/Basic.lean +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -27,12 +27,13 @@ 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. `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. +implies its uniform counterpart. `IndistinguishableWithAdvice advice` and +`InversionHardWithAdvice f advice` fix one advice family; with empty advice they are exactly the +uniform notions, 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`, +`InversionHardWithAdvice.inversion_negligible_encoded`): an adversary need not decode its advice, +since it may run on the encoded word exactly as on the typed value. These are definitions, not assertions that such primitives exist. @@ -42,6 +43,8 @@ These are definitions, not assertions that such primitives exist. tests given one fixed advice family. * `Cslib.Crypto.NonuniformlyIndistinguishable`: indistinguishability with every polynomially bounded advice family. +* `Cslib.Crypto.InversionHardWithAdvice`: hardness of inversion against uniform strict PPT + inverters given one fixed advice family. * `Cslib.Crypto.NonuniformOneWay`: one-wayness against inverters given polynomially bounded advice. * `Cslib.Crypto.NonuniformPRG`: a stretching generator whose output is nonuniformly @@ -60,7 +63,9 @@ These are definitions, not assertions that such primitives exist. 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.InversionHardWithAdvice.inversion_negligible_encoded`: advice of any encoded type. +* `Cslib.Crypto.oneWay_iff_inversionHardWithAdvice_nil`: uniform one-wayness is hardness of + inversion with empty advice. * `Cslib.Crypto.not_computationallyIndistinguishable_pure_uniformList`, `Cslib.Crypto.not_nonuniformlyIndistinguishable_pure_uniformList`: fixed words are distinguishable from uniform words, so the indistinguishability notions are not trivially true. @@ -219,51 +224,45 @@ theorem not_nonuniformlyIndistinguishable_pure_uniformList (target : ℕ → Lis not_computationallyIndistinguishable_pure_uniformList target hlength h.computationallyIndistinguishable -/-- A function is **nonuniformly one-way** when one deterministic polynomial-time algorithm -evaluates it and, for every polynomially bounded advice family, each uniform strict PPT inverter -reading the parameter, the advice word and the image has negligible probability of finding any -preimage of a uniform input. -/ -structure NonuniformOneWay (f : List Bool → List Bool) : Prop where - /-- A deterministic polynomial-time algorithm evaluates the function. -/ - polyTime : ComputableInPolyTime f encBits encBits - /-- With each polynomially bounded advice family, inversion is indistinguishable from certain - failure. -/ - secure : ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → - Game.Indistinguishable - (fun (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) n => - ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n)) - (fun _ _ => PMF.pure false) (IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits) - -/-- Each efficient inverter with polynomially bounded advice has negligible success. -/ -theorem NonuniformOneWay.inversion_negligible {f : List Bool → List Bool} - (h : NonuniformOneWay f) (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) - (hPPT : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary) - {advice : ℕ → List Bool} (hadvice : PolynomiallyBounded (fun n => (advice n).length)) : +/-- **Inversion of `f` is hard with advice** `advice` when each uniform strict PPT inverter +reading the parameter `n`, the advice word `advice n` and the image of a uniform `n`-bit input has +negligible probability of finding any preimage. The advice family is not bounded here; its length +is charged to the inverter's clock. With empty advice this is the security condition of `OneWay` +(`oneWay_iff_inversionHardWithAdvice_nil`). -/ +def InversionHardWithAdvice (f : List Bool → List Bool) (advice : ℕ → List Bool) : Prop := + Game.Indistinguishable + (fun (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) n => + ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n)) + (fun _ _ => PMF.pure false) (IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits) + +/-- Each efficient inverter with the given advice has negligible success. -/ +theorem InversionHardWithAdvice.inversion_negligible {f : List Bool → List Bool} + {advice : ℕ → List Bool} (h : InversionHardWithAdvice f advice) + (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) + (hPPT : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary) : Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n))) := by - simpa only [Game.advantage_pure_false] using h.secure advice hadvice adversary hPPT + simpa only [Game.advantage_pure_false] using h adversary hPPT -/-- Establish nonuniform one-wayness by bounding the success probability of every efficient -inverter with polynomially bounded advice. -/ -theorem NonuniformOneWay.of_inversion_negligible {f : List Bool → List Bool} - (hf : ComputableInPolyTime f encBits encBits) +/-- Establish hardness with advice by bounding every efficient inverter's success +probability. -/ +theorem InversionHardWithAdvice.of_inversion_negligible {f : List Bool → List Bool} + {advice : ℕ → List Bool} (h : ∀ adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool), IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary → - ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n)))) : - NonuniformOneWay f := by - refine ⟨hf, fun advice hadvice adversary hPPT => ?_⟩ - simpa only [Game.advantage_pure_false] using h adversary hPPT advice hadvice - -/-- **Advice of any encoded type.** A nonuniformly one-way function resists every uniform strict -PPT inverter reading an advice value of an arbitrary type, under an arbitrary encoding with -polynomially bounded lengths. -/ -theorem NonuniformOneWay.inversion_negligible_encoded {f : List Bool → List Bool} - (h : NonuniformOneWay f) {γ : Type} {encAdvice : γ ↪ List Bool} + InversionHardWithAdvice f advice := fun adversary hPPT => by + simpa only [Game.advantage_pure_false] using h adversary hPPT + +/-- **Advice of any encoded type.** Hardness with the advice words `encAdvice (advice n)` covers +every uniform strict PPT inverter that reads the advice value `advice n` itself, of an arbitrary +type under an arbitrary encoding. -/ +theorem InversionHardWithAdvice.inversion_negligible_encoded {f : List Bool → List Bool} + {γ : Type} {encAdvice : γ ↪ List Bool} {advice : ℕ → γ} + (h : InversionHardWithAdvice f (fun n => encAdvice (advice n))) {adversary : (ℕ × γ) × List Bool → ProbComp (List Bool)} - (hPPT : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBits adversary) - {advice : ℕ → γ} (hadvice : PolynomiallyBounded (fun n => (encAdvice (advice n)).length)) : + (hPPT : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBits adversary) : Negligible (fun n => Game.succProbability (ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n))) := by obtain ⟨extension, hextension, heq⟩ := @@ -280,16 +279,62 @@ theorem NonuniformOneWay.inversion_negligible_encoded {f : List Bool → List Bo (encPair (encPair encUnary encBits) encBits ((n, encAdvice (advice n)), image))) n) = ProbComp.eval (inversionGame f (fun n image => adversary ((n, advice n), image)) n) := by simp only [inversionGame, ProbComp.eval_bind, hkey] - simpa only [hgame] using h.inversion_negligible _ hword hadvice + simpa only [hgame] using h.inversion_negligible _ hword + +/-- **Uniform one-wayness is the empty-advice case.** A uniform inverter is an advice inverter +that ignores its advice, and an advice inverter run on empty advice is a uniform inverter. -/ +theorem oneWay_iff_inversionHardWithAdvice_nil {f : List Bool → List Bool} : + OneWay f ↔ + ComputableInPolyTime f encBits encBits ∧ InversionHardWithAdvice f (fun _ => []) := by + constructor + · intro h + refine ⟨h.polyTime, .of_inversion_negligible fun adversary hPPT => ?_⟩ + have hprepare : ComputableInPolyTime (fun input : ℕ × List Bool => ((input.1, []), input.2)) + (encPair encUnary encBits) (encPair (encPair encUnary encBits) encBits) := by fun_prop + exact h.inversion_negligible (fun n image => adversary ((n, []), image)) + (hPPT.preprocess hprepare) + · rintro ⟨hf, h⟩ + refine OneWay.of_inversion_negligible hf fun adversary hPPT => ?_ + have hneg := h.inversion_negligible (fun input => adversary input.1.1 input.2) + (isPPTOn_dropAdvice hPPT) + simpa only using hneg + +/-- A function is **nonuniformly one-way** when one deterministic polynomial-time algorithm +evaluates it and inversion is hard with every polynomially bounded advice family. -/ +structure NonuniformOneWay (f : List Bool → List Bool) : Prop where + /-- A deterministic polynomial-time algorithm evaluates the function. -/ + polyTime : ComputableInPolyTime f encBits encBits + /-- With each polynomially bounded advice family, inversion is hard. -/ + secure : ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → + InversionHardWithAdvice f advice + +/-- Each efficient inverter with polynomially bounded advice has negligible success. -/ +theorem NonuniformOneWay.inversion_negligible {f : List Bool → List Bool} + (h : NonuniformOneWay f) (adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool)) + (hPPT : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary) + {advice : ℕ → List Bool} (hadvice : PolynomiallyBounded (fun n => (advice n).length)) : + Negligible (fun n => Game.succProbability (ProbComp.eval + (inversionGame f (fun n image => adversary ((n, advice n), image)) n))) := + (h.secure advice hadvice).inversion_negligible adversary hPPT + +/-- Establish nonuniform one-wayness by bounding the success probability of every efficient +inverter with polynomially bounded advice. -/ +theorem NonuniformOneWay.of_inversion_negligible {f : List Bool → List Bool} + (hf : ComputableInPolyTime f encBits encBits) + (h : ∀ adversary : (ℕ × List Bool) × List Bool → ProbComp (List Bool), + IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits adversary → + ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → + Negligible (fun n => Game.succProbability (ProbComp.eval + (inversionGame f (fun n image => adversary ((n, advice n), image)) n)))) : + NonuniformOneWay f := + ⟨hf, fun advice hadvice => + .of_inversion_negligible fun adversary hPPT => h adversary hPPT advice hadvice⟩ /-- Nonuniform one-wayness implies uniform one-wayness: a uniform inverter ignores empty advice. -/ theorem NonuniformOneWay.toOneWay {f : List Bool → List Bool} (h : NonuniformOneWay f) : - OneWay f := by - refine OneWay.of_inversion_negligible h.polyTime fun adversary hPPT => ?_ - have hneg := h.inversion_negligible (fun input => adversary input.1.1 input.2) - (isPPTOn_dropAdvice hPPT) (advice := fun _ => []) (PolynomiallyBounded.const 0) - simpa only using hneg + OneWay f := + oneWay_iff_inversionHardWithAdvice_nil.mpr ⟨h.polyTime, h.secure _ (PolynomiallyBounded.const 0)⟩ /-- A **nonuniform pseudorandom generator**: a plain polynomial-time generator with exact output length `length`, strictly expanding every seed length, whose output on a uniform seed is diff --git a/Complexity/Crypto/Computational/OneWay/Normalize.lean b/Complexity/Crypto/Computational/OneWay/Normalize.lean index 4e9a651799..993086580d 100644 --- a/Complexity/Crypto/Computational/OneWay/Normalize.lean +++ b/Complexity/Crypto/Computational/OneWay/Normalize.lean @@ -7,6 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate +public import Complexity.Crypto.Computational.Nonuniform.Basic public import Complexity.Crypto.Computational.OneWay public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.Padding import Complexity.Probability.PMF.Bind @@ -19,7 +20,8 @@ import Complexity.Tactic.PPT Self-delimiting padding using an output-size bound makes the output length depend only on the input length. Equality of padded images implies equality of the original images, even for a -candidate of a different length. A uniform strict PPT reduction therefore preserves one-wayness. +candidate of a different length. A uniform strict PPT reduction, which passes any advice through +unchanged, therefore preserves one-wayness, uniform or nonuniform. This supplies the fixed-output-width interface used by the pseudoentropy construction without assuming that the original function is length-preserving, injective or regular. @@ -29,9 +31,13 @@ assuming that the original function is length-preserving, injective or regular. ## Main results -* `Cslib.Crypto.OneWay.normalize`: output normalization preserves one-wayness. -* `Cslib.Crypto.OneWay.exists_fixedOutputLength`: every OWF yields an OWF with - a uniformly polynomial-time output-length function. +* `Cslib.Crypto.InversionHardWithAdvice.normalize`: output normalization preserves hardness of + inversion with any fixed advice family. +* `Cslib.Crypto.OneWay.normalize`, `Cslib.Crypto.NonuniformOneWay.normalize`: output + normalization preserves uniform and nonuniform one-wayness. +* `Cslib.Crypto.OneWay.exists_fixedOutputLength`, + `Cslib.Crypto.NonuniformOneWay.exists_fixedOutputLength`: every (nonuniform) OWF yields one + with a uniformly polynomial-time output-length function. ## References @@ -40,7 +46,7 @@ assuming that the original function is length-preserving, injective or regular. Adapted from Crypto/Computational/OneWay/Normalize.lean on the cslib `crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203ccd8`. This is the word-encoding reduction to the write-up's -fixed-output-width setting, using the shared tidy machine calculus and nonnegative game API. +fixed-output-width setting, using plain polynomial-time certificates and the nonnegative game API. -/ @[expose] public section @@ -86,19 +92,44 @@ theorem inversion_le (f : List Bool → List Bool) (bound : ℕ → ℕ) (advers end OneWayNormalization +/-- **Normalization relative to fixed advice.** Self-delimiting output padding preserves hardness +of inversion with any fixed advice family: the reduction pads its challenge and passes the advice +through. Uniform one-wayness (`OneWay.normalize`) is the empty-advice case. -/ +theorem InversionHardWithAdvice.normalize {f : List Bool → List Bool} {advice : ℕ → List Bool} + (h : InversionHardWithAdvice f advice) (bound : ℕ → ℕ) + (hbound : ComputableInPolyTime bound encUnary encUnary) : + InversionHardWithAdvice (OneWayNormalization.normalize f bound) advice := by + refine .of_inversion_negligible fun adversary hPPT => ?_ + have hprepare : ComputableInPolyTime + (fun ((n, word), image) => ((n, word), BitString.padWord (bound n) image)) + (encPair (encPair encUnary encBits) encBits) + (encPair (encPair encUnary encBits) encBits) := by fun_prop + exact negligible_of_le (h.inversion_negligible _ (hPPT.preprocess hprepare)) + (OneWayNormalization.inversion_le f bound (fun n image => adversary ((n, advice n), image))) + /-- Self-delimiting output padding preserves one-wayness against uniform strict PPT inverters. -/ theorem OneWay.normalize {f : List Bool → List Bool} (hf : OneWay f) (bound : ℕ → ℕ) (hbound : ComputableInPolyTime bound encUnary encUnary) : OneWay (OneWayNormalization.normalize f bound) := by - have hbound := hbound.tidy - apply OneWay.of_inversion_negligible - (.of_tidy <| - (OneWayNormalization.computableInPolyTime_normalize hf.polyTime (.of_tidy hbound)).tidy) - intro adversary hPPT - have hreduce : IsPPT encBits (fun n image => - adversary n (BitString.padWord (bound n) image)) := by ppt - exact negligible_of_le (hf.inversion_negligible _ hreduce) - (OneWayNormalization.inversion_le f bound adversary) + obtain ⟨hpoly, hhard⟩ := oneWay_iff_inversionHardWithAdvice_nil.mp hf + exact oneWay_iff_inversionHardWithAdvice_nil.mpr + ⟨OneWayNormalization.computableInPolyTime_normalize hpoly hbound, hhard.normalize bound hbound⟩ + +/-- Self-delimiting output padding preserves nonuniform one-wayness. -/ +theorem NonuniformOneWay.normalize {f : List Bool → List Bool} (hf : NonuniformOneWay f) + (bound : ℕ → ℕ) (hbound : ComputableInPolyTime bound encUnary encUnary) : + NonuniformOneWay (OneWayNormalization.normalize f bound) := + ⟨OneWayNormalization.computableInPolyTime_normalize hf.polyTime hbound, + fun advice hadvice => (hf.secure advice hadvice).normalize bound hbound⟩ + +/-- The output-size bound used to normalize an efficient function: a polynomial dominating its +output length. -/ +private theorem exists_normalizationBound {f : List Bool → List Bool} + (hf : ComputableInPolyTime f encBits encBits) : + ∃ bound : ℕ → ℕ, ComputableInPolyTime bound encUnary encUnary ∧ + ∀ input, (f input).length ≤ bound input.length := by + obtain ⟨c, d, hsize⟩ := hf.polyBounded_length.exists_le + exact ⟨fun n => c * (n + 1) ^ d, by fun_prop, hsize⟩ /-- Every OWF yields an OWF whose output length depends only on the input length. Both evaluation and this unary output-length function are uniformly polynomial time. -/ @@ -106,15 +137,19 @@ theorem OneWay.exists_fixedOutputLength {f : List Bool → List Bool} (hf : OneW ∃ (g : List Bool → List Bool) (length : ℕ → ℕ), OneWay g ∧ (∀ input, (g input).length = length input.length) ∧ ComputableInPolyTime length encUnary encUnary := by - simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] - obtain ⟨c, d, hsize⟩ := hf.polyTime.polyBounded_length.exists_le - let bound (n : ℕ) := c * (n + 1) ^ d - have hbound : ComputableTidilyInPolyTime bound encUnary encUnary := by - unfold bound - fun_prop - refine ⟨OneWayNormalization.normalize f bound, fun n => 2 * bound n + 1, - hf.normalize bound (.of_tidy hbound), ?_, by fun_prop⟩ - intro input - exact BitString.length_padWord (hsize input) + obtain ⟨bound, hbound, hsize⟩ := exists_normalizationBound hf.polyTime + exact ⟨OneWayNormalization.normalize f bound, fun n => 2 * bound n + 1, + hf.normalize bound hbound, fun input => BitString.length_padWord (hsize input), by fun_prop⟩ + +/-- Every nonuniform OWF yields a nonuniform OWF whose output length depends only on the input +length, with a uniformly polynomial-time output-length function. -/ +theorem NonuniformOneWay.exists_fixedOutputLength {f : List Bool → List Bool} + (hf : NonuniformOneWay f) : + ∃ (g : List Bool → List Bool) (length : ℕ → ℕ), NonuniformOneWay g ∧ + (∀ input, (g input).length = length input.length) ∧ + ComputableInPolyTime length encUnary encUnary := by + obtain ⟨bound, hbound, hsize⟩ := exists_normalizationBound hf.polyTime + exact ⟨OneWayNormalization.normalize f bound, fun n => 2 * bound n + 1, + hf.normalize bound hbound, fun input => BitString.length_padWord (hsize input), by fun_prop⟩ end Cslib.Crypto diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean b/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean index ba60137350..8b17256322 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Basic.lean @@ -32,11 +32,15 @@ strict PPT sampler's fair-bit tape as a uniform seed, including unused randomnes * `Cslib.Crypto.Pseudoentropy.predictionGame`: predict a sampled hidden bit from its observation. * `Cslib.Crypto.Pseudoentropy.SamplablePair`: a finite joint law with a uniform strict PPT sampler. * `Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap`: the conditional-entropy prediction threshold. +* `Cslib.Crypto.Pseudoentropy.SamplablePair.HasGapWithAdvice`: the same threshold against + predictors given one fixed advice family. ## Main results * `Cslib.Crypto.Pseudoentropy.isPPTOn_predictionGame`: the prediction experiment is strict PPT. * `Cslib.Crypto.Pseudoentropy.SamplablePair.eval_latentSample`: recover the exact latent joint law. +* `Cslib.Crypto.Pseudoentropy.SamplablePair.hasGap_iff_hasGapWithAdvice_nil`: the uniform gap is + the empty-advice case. * `Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_error_ge`: prediction error bound. * `Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_entropy_add_gap_le_one`: the threshold forced by an independent fair-bit predictor. @@ -121,6 +125,40 @@ def HasGap (pair : SamplablePair) (gap : ℕ → ℝ) : Prop := ∀ᶠ n in atTop, 2 * Pr[predictionGame pair.sample adversary n] - 1 ≤ 1 - PMF.conditionalEntropy (pair.joint n) - gap n +/-- **The prediction gap relative to fixed advice**: every uniform strict PPT predictor that also +reads the advice word `advice n` stays below the conditional-entropy threshold by `gap`. The advice +family is not bounded here; its length is charged to the predictor's clock. With empty advice this +is `HasGap` (`hasGap_iff_hasGapWithAdvice_nil`). -/ +def HasGapWithAdvice (pair : SamplablePair) (gap : ℕ → ℝ) (advice : ℕ → List Bool) : Prop := + ∀ adversary : (ℕ × List Bool) × List Bool → ProbComp Bool, + IsPPTOn (encPair (encPair encUnary encBits) encBits) encBool adversary → + ∀ᶠ n in atTop, + 2 * Pr[predictionGame pair.sample (fun n word => adversary ((n, advice n), word)) n] - 1 ≤ + 1 - PMF.conditionalEntropy (pair.joint n) - gap n + +/-- **The uniform gap is the empty-advice case.** A uniform predictor is an advice predictor that +ignores its advice, and an advice predictor run on empty advice is a uniform predictor. -/ +theorem hasGap_iff_hasGapWithAdvice_nil {pair : SamplablePair} {gap : ℕ → ℝ} : + pair.HasGap gap ↔ pair.HasGapWithAdvice gap (fun _ => []) := by + constructor + · intro h adversary hadversary + have hprepare : ComputableInPolyTime (fun (n, word) => ((n, ([] : List Bool)), word)) + (encPair encUnary encBits) (encPair (encPair encUnary encBits) encBits) := by fun_prop + exact h (fun n word => adversary ((n, []), word)) (hadversary.preprocess hprepare) + · intro h adversary hadversary + have hprepare : ComputableInPolyTime + (fun ((n, _), word) => (n, word) : (ℕ × List Bool) × List Bool → ℕ × List Bool) + (encPair (encPair encUnary encBits) encBits) (encPair encUnary encBits) := by fun_prop + exact h (fun ((n, _), word) => adversary n word) (hadversary.on.preprocess hprepare) + +/-- A smaller requested gap follows from any larger proved gap, with the same advice. -/ +theorem HasGapWithAdvice.mono {pair : SamplablePair} {gap smaller : ℕ → ℝ} + {advice : ℕ → List Bool} (h : pair.HasGapWithAdvice gap advice) + (hle : ∀ n, smaller n ≤ gap n) : pair.HasGapWithAdvice smaller advice := by + intro adversary hPPT + filter_upwards [h adversary hPPT] with n hn + exact hn.trans (sub_le_sub_left (hle n) _) + /-- The pseudoentropy threshold equivalently lower-bounds each efficient predictor's error. -/ theorem HasGap.eventually_error_ge {pair : SamplablePair} {gap : ℕ → ℝ} (hgap : pair.HasGap gap) (adversary : Distinguisher) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean index cbbe08c7c8..ca7eb41afd 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean @@ -9,30 +9,38 @@ module public import Complexity.Crypto.Computational.Pseudoentropy.WordReduction import Complexity.Languages.Probabilistic.Notation -import Complexity.Crypto.Computational.OneWay.Normalize +public import Complexity.Crypto.Computational.OneWay.Normalize import Complexity.Computability.Probabilistic.CoinTape import Complexity.Crypto.Negligible.Basic +import Complexity.Computability.Probabilistic.PPT.Composition /-! # The pseudoentropy prediction gap from one-wayness The executable hashed parity reduction has polynomial loss. One-wayness therefore makes its inversion term negligible, leaving an inverse-polynomial gap between feasible prediction and -the entropy threshold. Each predictor supplies one inverter with a fixed precision degree; -neither its code nor its choice of saved randomness depends on a nonuniform advice string. +the entropy threshold. Each predictor supplies one inverter with a fixed precision degree. The +argument is stated relative to a fixed advice family: a predictor reading advice gives an inverter +reading the same advice, and the advice length costs only a polynomial change of coin budget. The +uniform theorems are the empty-advice case. ## Main results +* `Cslib.Crypto.Pseudoentropy.HashPair.eventually_prediction_entropy_le_withAdvice`, + `Cslib.Crypto.Pseudoentropy.HashPair.pair_hasGapWithAdvice`: the prediction gap relative to a + fixed advice family. * `Cslib.Crypto.Pseudoentropy.HashPair.pair_hasGap`: prediction gap for normalized word functions. -* `Cslib.Crypto.OneWay.exists_pseudoentropyPair`: every uniform OWF gives an exactly samplable - pair with an inverse-linear prediction gap, including variable-length original images. +* `Cslib.Crypto.OneWay.exists_pseudoentropyPair`, + `Cslib.Crypto.NonuniformOneWay.exists_pseudoentropyPair`: every uniform (nonuniform) OWF gives + an exactly samplable pair with an inverse-linear prediction gap against uniform predictors + (predictors with polynomially bounded advice), including variable-length original images. ## References * [T. Holenstein, *Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness*][Holenstein2006], Definition 4 and Section 4, Lemmas 3 and 4. We use the public matrix and dyadic-range variant proved in `HashReduction`. This module - discharges the inversion hypothesis using uniform strict PPT one-wayness. + discharges the inversion hypothesis using hardness of inversion with fixed advice. Adapted from Crypto/Computational/Pseudoentropy/OneWay.lean on the cslib `crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203ccd8`, using typed saved seeds and nonnegative security games. @@ -54,23 +62,75 @@ theorem precision_three_ge {n : ℕ} (hn : 8 ≤ n) : simp only [precision, pow_succ] at * nlinarith -/-- The finite entropy threshold holds eventually against every uniform PPT word predictor. -The image may have any fixed width at each parameter; it need not be a permutation or regular. -/ -theorem eventually_prediction_entropy_le {f : List Bool → List Bool} (hf : OneWay f) +/-- A polynomially bounded advice family costs only a polynomial factor in the clock: a budget +polynomial in the advice-carrying encoding is dominated by one polynomial in the encoding of the +parameter and word alone. -/ +private theorem exists_advice_budget_le {advice : ℕ → List Bool} + (hadvice : PolynomiallyBounded (fun n => (advice n).length)) (c d : ℕ) : + ∃ c' d' : ℕ, ∀ n word, + c * ((encPair (encPair encUnary encBits) encBits ((n, advice n), word)).length + 1) ^ d ≤ + c' * ((encPair encUnary encBits (n, word)).length + 1) ^ d' := by + obtain ⟨C, D, hC⟩ := polynomiallyBounded_iff_le.mp hadvice + refine ⟨c * (2 * C + 4) ^ d, (D + 1) * d, fun n word => ?_⟩ + simp only [length_encPair, encUnary_apply, List.length_replicate, encBits_apply] + set L := 2 * n + 1 + word.length + 1 with hL + have hL1 : 1 ≤ L := by omega + have hnL : n + 1 ≤ L := by omega + have hpow : (n + 1) ^ D ≤ L ^ D := Nat.pow_le_pow_left hnL D + have hLD : L ≤ L ^ (D + 1) := by + calc L = L ^ 1 := (pow_one L).symm + _ ≤ L ^ (D + 1) := Nat.pow_le_pow_right hL1 (by omega) + have hLD' : L ^ D ≤ L ^ (D + 1) := Nat.pow_le_pow_right hL1 (by omega) + have hbase : 2 * (2 * n + 1 + (advice n).length) + 1 + word.length + 1 ≤ + (2 * C + 4) * L ^ (D + 1) := by + have := hC n + nlinarith + calc c * (2 * (2 * n + 1 + (advice n).length) + 1 + word.length + 1) ^ d + ≤ c * ((2 * C + 4) * L ^ (D + 1)) ^ d := Nat.mul_le_mul_left c (Nat.pow_le_pow_left hbase d) + _ = c * (2 * C + 4) ^ d * L ^ ((D + 1) * d) := by rw [mul_pow, ← pow_mul, mul_assoc] + +/-- **The prediction gap relative to fixed advice.** If inverting `f` is hard with a polynomially +bounded advice family, then every uniform strict PPT word predictor reading the same advice +eventually stays below the finite entropy threshold. The hashed-parity reduction turns the +predictor into an inverter that passes its advice through; the advice length enters only a +polynomial change of the predictor's coin budget. -/ +theorem eventually_prediction_entropy_le_withAdvice {f : List Bool → List Bool} + (hf : ComputableInPolyTime f encBits encBits) {advice : ℕ → List Bool} + (hhard : InversionHardWithAdvice f advice) + (hadvice : PolynomiallyBounded (fun n => (advice n).length)) {Image : ℕ → Type} [∀ n, Finite (Image n)] (finiteFunction : ∀ n, BitString n → Image n) (encodeImage : ∀ n, Image n ↪ List Bool) (hencode : ∀ n x, f (List.ofFn x) = encodeImage n (finiteFunction n x)) (imageLength : ℕ → ℕ) (hlength : ∀ n image, (encodeImage n image).length = imageLength n) - (adversary : Distinguisher) (hPPT : IsPPT encBool adversary) : - ∀ᶠ n in atTop, 2 * Pr[predictionGame (sample f) adversary n] - 1 ≤ + (adversary : (ℕ × List Bool) × List Bool → ProbComp Bool) + (hPPT : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBool adversary) : + ∀ᶠ n in atTop, 2 * Pr[predictionGame (sample f) + (fun n word => adversary ((n, advice n), word)) n] - 1 ≤ 1 - PMF.conditionalEntropy (joint (count := hashCount n) (finiteFunction n)) - 1 / (hashCount n : ℝ) := by - obtain ⟨c, d, evaluate, hefficient, _, hrealize⟩ := hPPT.on.exists_total_seeded_evaluator - have hinversion := hf.inversion_negligible _ - (isPPT_wordInverter hf.polyTime hefficient c d 3) + obtain ⟨c, d, evaluate, hefficient, _, hrealize⟩ := hPPT.exists_total_seeded_evaluator + obtain ⟨c', d', hbudget⟩ := exists_advice_budget_le hadvice c d + -- The inverter captures the advice word from its own input. + let advisedEvaluate : (ℕ × List Bool) × List Bool → (ℕ × List Bool) → List Bool → Bool := + fun ((_, word), _) (m, observation) coins => evaluate ((m, word), observation) coins + have hevaluate : ComputableInPolyTime + (fun ((a, observation), tape) => advisedEvaluate a observation tape) + (encPair (encPair (encPair (encPair encUnary encBits) encBits) (encPair encUnary encBits)) + encBits) encBool := + hefficient.comp (show ComputableInPolyTime + (fun ((((_, word), _), (m, observation)), tape) => (((m, word), observation), tape) : + (((ℕ × List Bool) × List Bool) × (ℕ × List Bool)) × List Bool → + ((ℕ × List Bool) × List Bool) × List Bool) + (encPair (encPair (encPair (encPair encUnary encBits) encBits) (encPair encUnary encBits)) + encBits) (encPair (encPair (encPair encUnary encBits) encBits) encBits) by fun_prop) + have hinverter := isPPTOn_wordInverter (evaluate := advisedEvaluate) + (parameter := fun ((n, _), _) => n) (image := fun ((_, _), image) => image) hf hevaluate + (by fun_prop) (by fun_prop) c' d' 3 + have hinversion := hhard.inversion_negligible _ hinverter have hloss : Negligible (fun n => 128 * (dyadicSize (16 * hashCount n) : ℝ≥0) ^ 2 * - Game.succProbability - (ProbComp.eval (inversionGame f (wordInverter f evaluate c d 3) n))) := by + Game.succProbability (ProbComp.eval (inversionGame f + (fun n image => wordInverter f (advisedEvaluate ((n, advice n), image)) c' d' 3 n image) + n))) := by simpa only [Nat.cast_mul, Nat.cast_ofNat, Nat.cast_pow] using hinversion.polynomiallyBounded_mul (show PolynomiallyBounded (fun n => 128 * dyadicSize (16 * hashCount n) ^ 2) by fun_prop) @@ -80,12 +140,55 @@ theorem eventually_prediction_entropy_le {f : List Bool → List Bool} (hf : One simp only [NNReal.coe_mul, NNReal.coe_pow, NNReal.coe_ofNat, NNReal.coe_natCast, Game.coe_succProbability] at hsmall have h := word_prediction_entropy_le f (finiteFunction n) (encodeImage n) - (hencode n) (hlength n) adversary evaluate c d (fun n input => hrealize (n, input)) + (hencode n) (hlength n) (fun n word => adversary ((n, advice n), word)) + (fun (m, word) coins => evaluate ((m, advice m), word) coins) c' d' + (fun m word budget hle => hrealize ((m, advice m), word) budget ((hbudget m word).trans hle)) 3 (precision_three_ge hn) have htwo : (2 : ℝ) / hashCount n = 2 * (1 / (hashCount n : ℝ)) := by ring rw [htwo] at h + have hsame : Pr[inversionGame f (wordInverter f + (fun (m, word) coins => evaluate ((m, advice m), word) coins) c' d' 3) n] = + Pr[inversionGame f (fun n image => + wordInverter f (advisedEvaluate ((n, advice n), image)) c' d' 3 n image) n] := rfl + rw [hsame] at h linarith +/-- The finite entropy threshold holds eventually against every uniform PPT word predictor. +The image may have any fixed width at each parameter; it need not be a permutation or regular. +This is the empty-advice case of `eventually_prediction_entropy_le_withAdvice`. -/ +theorem eventually_prediction_entropy_le {f : List Bool → List Bool} (hf : OneWay f) + {Image : ℕ → Type} [∀ n, Finite (Image n)] + (finiteFunction : ∀ n, BitString n → Image n) (encodeImage : ∀ n, Image n ↪ List Bool) + (hencode : ∀ n x, f (List.ofFn x) = encodeImage n (finiteFunction n x)) + (imageLength : ℕ → ℕ) (hlength : ∀ n image, (encodeImage n image).length = imageLength n) + (adversary : Distinguisher) (hPPT : IsPPT encBool adversary) : + ∀ᶠ n in atTop, 2 * Pr[predictionGame (sample f) adversary n] - 1 ≤ + 1 - PMF.conditionalEntropy (joint (count := hashCount n) (finiteFunction n)) - + 1 / (hashCount n : ℝ) := by + obtain ⟨hpoly, hhard⟩ := oneWay_iff_inversionHardWithAdvice_nil.mp hf + have hprepare : ComputableInPolyTime + (fun ((n, _), word) => (n, word) : (ℕ × List Bool) × List Bool → ℕ × List Bool) + (encPair (encPair encUnary encBits) encBits) (encPair encUnary encBits) := by fun_prop + exact eventually_prediction_entropy_le_withAdvice hpoly hhard (PolynomiallyBounded.const 0) + finiteFunction encodeImage hencode imageLength hlength + (fun ((n, _), word) => adversary n word) (hPPT.on.preprocess hprepare) + +/-- A function whose inversion is hard with a polynomially bounded advice family, and which has a +fixed image width at each parameter, gives a samplable pair whose gap holds against predictors with +the same advice. The gap is inverse-linear in the original input length. -/ +theorem pair_hasGapWithAdvice {f : List Bool → List Bool} + (hf : ComputableInPolyTime f encBits encBits) {advice : ℕ → List Bool} + (hhard : InversionHardWithAdvice f advice) + (hadvice : PolynomiallyBounded (fun n => (advice n).length)) + {Image : ℕ → Type} [∀ n, Finite (Image n)] + (finiteFunction : ∀ n, BitString n → Image n) (encodeImage : ∀ n, Image n ↪ List Bool) + (hencode : ∀ n x, f (List.ofFn x) = encodeImage n (finiteFunction n x)) + (imageLength : ℕ → ℕ) (hlength : ∀ n image, (encodeImage n image).length = imageLength n) : + (pair f hf finiteFunction encodeImage hencode).HasGapWithAdvice + (fun n => 1 / (hashCount n : ℝ)) advice := + eventually_prediction_entropy_le_withAdvice hf hhard hadvice finiteFunction encodeImage hencode + imageLength hlength + /-- A one-way function with a fixed image width at each parameter gives a samplable pseudoentropy pair. The gap is inverse-linear in the original input length. -/ theorem pair_hasGap {f : List Bool → List Bool} (hf : OneWay f) @@ -103,23 +206,47 @@ namespace Cslib.Crypto open Probability BitString Pseudoentropy Turing.MultiTapeTM -/-- Every one-way word function yields an exactly samplable pseudoentropy pair with an explicit -inverse-polynomial prediction gap. Normalization handles arbitrary original output lengths. -/ -theorem OneWay.exists_pseudoentropyPair {f : List Bool → List Bool} (hf : OneWay f) : - ∃ pair : SamplablePair, pair.HasGap (fun n => 1 / (2 * ((n : ℝ) + 7))) := by - obtain ⟨g, length, hg, hlength, _⟩ := hf.exists_fixedOutputLength +/-- The samplable pair of a function with a fixed output length: its gap holds against predictors +with any polynomially bounded advice family for which inverting the function is hard. -/ +private theorem exists_pseudoentropyPair_of_fixedOutputLength {g : List Bool → List Bool} + {length : ℕ → ℕ} (hg : ComputableInPolyTime g encBits encBits) + (hlength : ∀ input, (g input).length = length input.length) : + ∃ pair : SamplablePair, ∀ advice : ℕ → List Bool, InversionHardWithAdvice g advice → + PolynomiallyBounded (fun n => (advice n).length) → + pair.HasGapWithAdvice (fun n => 1 / (2 * ((n : ℝ) + 7))) advice := by let finiteFunction (n : ℕ) (x : BitString n) := ofList (length n) (g (List.ofFn x)) let encodeImage (n : ℕ) : BitString (length n) ↪ List Bool := ⟨List.ofFn, fun _ _ h => List.ofFn_inj.mp h⟩ have hencode (n : ℕ) (x : BitString n) : g (List.ofFn x) = encodeImage n (finiteFunction n x) := by exact (ofFn_ofList (by simp [hlength])).symm - refine ⟨HashPair.pair g hg.polyTime finiteFunction encodeImage hencode, - (HashPair.pair_hasGap hg finiteFunction encodeImage hencode length - (fun _ _ => List.length_ofFn)).mono - (fun n => ?_)⟩ + refine ⟨HashPair.pair g hg finiteFunction encodeImage hencode, fun advice hhard hadvice => + (HashPair.pair_hasGapWithAdvice hg hhard hadvice finiteFunction encodeImage hencode length + (fun _ _ => List.length_ofFn)).mono (fun n => ?_)⟩ apply one_div_le_one_div_of_le · exact_mod_cast Nat.pos_of_ne_zero (NeZero.ne (HashPair.hashCount n)) · exact_mod_cast HashPair.hashCount_le n +/-- Every one-way word function yields an exactly samplable pseudoentropy pair with an explicit +inverse-polynomial prediction gap. Normalization handles arbitrary original output lengths. -/ +theorem OneWay.exists_pseudoentropyPair {f : List Bool → List Bool} (hf : OneWay f) : + ∃ pair : SamplablePair, pair.HasGap (fun n => 1 / (2 * ((n : ℝ) + 7))) := by + obtain ⟨g, length, hg, hlength, _⟩ := hf.exists_fixedOutputLength + obtain ⟨hpoly, hhard⟩ := oneWay_iff_inversionHardWithAdvice_nil.mp hg + obtain ⟨pair, hpair⟩ := exists_pseudoentropyPair_of_fixedOutputLength hpoly hlength + exact ⟨pair, SamplablePair.hasGap_iff_hasGapWithAdvice_nil.mpr + (hpair _ hhard (PolynomiallyBounded.const 0))⟩ + +/-- Every nonuniformly one-way word function yields an exactly samplable pair whose +inverse-polynomial prediction gap holds against predictors with every polynomially bounded advice +family. -/ +theorem NonuniformOneWay.exists_pseudoentropyPair {f : List Bool → List Bool} + (hf : NonuniformOneWay f) : + ∃ pair : SamplablePair, ∀ advice : ℕ → List Bool, + PolynomiallyBounded (fun n => (advice n).length) → + pair.HasGapWithAdvice (fun n => 1 / (2 * ((n : ℝ) + 7))) advice := by + obtain ⟨g, length, hg, hlength, _⟩ := hf.exists_fixedOutputLength + obtain ⟨pair, hpair⟩ := exists_pseudoentropyPair_of_fixedOutputLength hg.polyTime hlength + exact ⟨pair, fun advice hadvice => hpair advice (hg.secure advice hadvice) hadvice⟩ + end Cslib.Crypto diff --git a/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean b/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean index 05ead3fab5..08a3b266b6 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/WordReduction.lean @@ -34,7 +34,8 @@ The saved evaluator returns a Boolean directly, without decoding arbitrary outpu ## Main results -* `Cslib.Crypto.Pseudoentropy.HashPair.isPPT_wordInverter`: strict uniform PPT. +* `Cslib.Crypto.Pseudoentropy.HashPair.isPPTOn_wordInverter`: strict uniform PPT, with the + evaluator, parameter and image computed from an arbitrary input. * `Cslib.Crypto.Pseudoentropy.HashPair.wordInverter_eval`: the exact finite/list law. * `Cslib.Crypto.Pseudoentropy.HashPair.word_prediction_entropy_le`: the complete reduction bound. @@ -75,15 +76,15 @@ def predictWithCoins (evaluate : (ℕ × List Bool) → List Bool → Bool) (n : (image : List Bool) (index : ℕ) (matrix digest coins query : List Bool) : Bool := evaluate (n, wordObservation image index matrix digest query) coins -/-- Captured public fields and coins use their ordinary efficiency certificates. The typed -callback has a uniformly polynomial bound on every supplied input, not only sampled words. -/ +/-- Captured public fields and coins use their ordinary efficiency certificates. The evaluator may +itself depend on the captured input, for example on an advice word. The typed callback has a +uniformly polynomial bound on every supplied input, not only sampled words. -/ @[fun_prop] theorem computableInPolyTime_predictWithCoins {α : Type} {encode : α ↪ List Bool} - {evaluate : (ℕ × List Bool) → List Bool → Bool} {parameter index : α → ℕ} + {evaluate : α → (ℕ × List Bool) → List Bool → Bool} {parameter index : α → ℕ} {image matrix digest coins query : α → List Bool} - (hevaluate : ComputableInPolyTime - (fun p : (ℕ × List Bool) × List Bool => evaluate p.1 p.2) - (encPair (encPair encUnary encBits) encBits) encBool) + (hevaluate : ComputableInPolyTime (fun ((a, observation), tape) => evaluate a observation tape) + (encPair (encPair encode (encPair encUnary encBits)) encBits) encBool) (hparameter : ComputableInPolyTime parameter encode encUnary) (himage : ComputableInPolyTime image encode encBits) (hindex : ComputableInPolyTime index encode encUnary) @@ -91,10 +92,15 @@ theorem computableInPolyTime_predictWithCoins {α : Type} {encode : α ↪ List (hdigest : ComputableInPolyTime digest encode encBits) (hcoins : ComputableInPolyTime coins encode encBits) (hquery : ComputableInPolyTime query encode encBits) : - ComputableInPolyTime (fun a => predictWithCoins evaluate (parameter a) (image a) + ComputableInPolyTime (fun a => predictWithCoins (evaluate a) (parameter a) (image a) (index a) (matrix a) (digest a) (coins a) (query a)) encode encBool := by unfold predictWithCoins - fun_prop + have harg : ComputableInPolyTime (fun a => ((a, (parameter a, wordObservation (image a) + (index a) (matrix a) (digest a) (query a))), coins a)) encode + (encPair (encPair encode (encPair encUnary encBits)) encBits) := + ((ComputableInPolyTime.of_eq fun _ => rfl).prod + (hparameter.prod (by fun_prop))).prod hcoins + exact hevaluate.comp harg /-- Guess the unknown hash value and decode, using the same predictor coins for every query. -/ noncomputable def wordInverter (f : List Bool → List Bool) @@ -107,38 +113,62 @@ noncomputable def wordInverter (f : List Bool → List Bool) return wordDecode f (predictWithCoins evaluate n image index matrix digest coins) degree n image masks -attribute [local fun_prop] ComputableInPolyTime.tidy in -/-- The complete inverter is one strict PPT program for every parameter and image. -/ +/-- **The inverter with a captured evaluator** is one strict PPT program on any input type: the +evaluator, parameter and image may all be computed from the input, which may carry an advice +word. -/ @[program_certificate] -theorem isPPT_wordInverter {f : List Bool → List Bool} - {evaluate : (ℕ × List Bool) → List Bool → Bool} +theorem isPPTOn_wordInverter {α : Type} {input : α ↪ List Bool} {f : List Bool → List Bool} + {evaluate : α → (ℕ × List Bool) → List Bool → Bool} {parameter : α → ℕ} + {image : α → List Bool} (hf : ComputableInPolyTime f encBits encBits) - (hevaluate : ComputableInPolyTime - (fun p : (ℕ × List Bool) × List Bool => evaluate p.1 p.2) - (encPair (encPair encUnary encBits) encBits) encBool) - (c d degree : ℕ) : IsPPT encBits (wordInverter f evaluate c d degree) := by - have hf := hf.tidy - have hevaluate := hevaluate.tidy - have hhash : ComputableTidilyInPolyTime hashCount encUnary encUnary := - (computableInPolyTime_hashCount (.of_tidy (by fun_prop))).tidy - have hbudget : ComputableTidilyInPolyTime - (fun a : ℕ × List Bool => coinBudget c d a.1 a.2.length) - (encPair encUnary encBits) encUnary := - (computableInPolyTime_coinBudget c d (.of_tidy (by fun_prop)) - (.of_tidy (by fun_prop))).tidy - have hdecode {β : Type} {encode : β ↪ List Bool} - {predictor : β → List Bool → Bool} {dimension : β → ℕ} {image masks : β → List Bool} - (hpredictor : ComputableTidilyInPolyTime (fun p : β × List Bool => predictor p.1 p.2) - (encPair encode encBits) encBool) - (hdimension : ComputableTidilyInPolyTime dimension encode encUnary) - (himage : ComputableTidilyInPolyTime image encode encBits) - (hmasks : ComputableTidilyInPolyTime masks encode encBits) : - ComputableTidilyInPolyTime (fun a => wordDecode f (predictor a) degree (dimension a) - (image a) (masks a)) encode encBits := - (polyTime_wordDecode degree (.of_tidy hf) (.of_tidy hpredictor) - (.of_tidy hdimension) (.of_tidy himage) (.of_tidy hmasks)).tidy - unfold wordInverter predictWithCoins - fun_prop + (hevaluate : ComputableInPolyTime (fun ((a, observation), tape) => evaluate a observation tape) + (encPair (encPair input (encPair encUnary encBits)) encBits) encBool) + (hparameter : ComputableInPolyTime parameter input encUnary) + (himage : ComputableInPolyTime image input encBits) (c d degree : ℕ) : + IsPPTOn input encBits + (fun a => wordInverter f (evaluate a) c d degree (parameter a) (image a)) := by + -- The five sampled values (coins, index, matrix, digest, masks) are kept alongside the input. + let e₅ := encPair (encPair (encPair (encPair (encPair input encBits) encUnary) encBits) encBits) + encBits + have hhash : ComputableInPolyTime hashCount encUnary encUnary := + computableInPolyTime_hashCount (by fun_prop) + have hinput : ComputableInPolyTime + (fun q : ((((α × List Bool) × ℕ) × List Bool) × List Bool) × List Bool => q.1.1.1.1.1) + e₅ input := by fun_prop + have hpredictor : ComputableInPolyTime + (fun p : (((((α × List Bool) × ℕ) × List Bool) × List Bool) × List Bool) × List Bool => + predictWithCoins (evaluate p.1.1.1.1.1.1) (parameter p.1.1.1.1.1.1) + (image p.1.1.1.1.1.1) p.1.1.1.1.2 p.1.1.1.2 p.1.1.2 p.1.1.1.1.1.2 p.2) + (encPair e₅ encBits) encBool := by + have hevaluate' : ComputableInPolyTime + (fun ((p, observation), tape) => evaluate p.1.1.1.1.1.1 observation tape : + ((((((((α × List Bool) × ℕ) × List Bool) × List Bool) × List Bool) × List Bool) × + (ℕ × List Bool)) × List Bool) → Bool) + (encPair (encPair (encPair e₅ encBits) (encPair encUnary encBits)) encBits) encBool := + hevaluate.comp (show ComputableInPolyTime + (fun ((p, observation), tape) => ((p.1.1.1.1.1.1, observation), tape) : + ((((((((α × List Bool) × ℕ) × List Bool) × List Bool) × List Bool) × List Bool) × + (ℕ × List Bool)) × List Bool) → (α × (ℕ × List Bool)) × List Bool) + (encPair (encPair (encPair e₅ encBits) (encPair encUnary encBits)) encBits) + (encPair (encPair input (encPair encUnary encBits)) encBits) by fun_prop) + exact computableInPolyTime_predictWithCoins hevaluate' (by fun_prop) (by fun_prop) + (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) (by fun_prop) + have hdecode : ComputableInPolyTime + (fun q : ((((α × List Bool) × ℕ) × List Bool) × List Bool) × List Bool => + wordDecode f (predictWithCoins (evaluate q.1.1.1.1.1) (parameter q.1.1.1.1.1) + (image q.1.1.1.1.1) q.1.1.1.2 q.1.1.2 q.1.2 q.1.1.1.1.2) degree + (parameter q.1.1.1.1.1) (image q.1.1.1.1.1) q.2) e₅ encBits := + polyTime_wordDecode degree hf hpredictor (hparameter.comp hinput) (himage.comp hinput) + (ComputableInPolyTime.snd _ _) + unfold wordInverter + refine IsPPTOn.bind_with (left := encBits) + (isPPTOn_sampleList.preprocess (computableInPolyTime_coinBudget c d hparameter + (by fun_prop))) ?_ + refine IsPPTOn.bind_with (left := encUnary) (isPPTOn_sampleDyadicIndex (by fun_prop)) ?_ + refine IsPPTOn.bind_with (left := encBits) (isPPTOn_sampleList.preprocess (by fun_prop)) ?_ + refine IsPPTOn.bind_with (left := encBits) (isPPTOn_sampleList.preprocess (by fun_prop)) ?_ + refine IsPPTOn.bind_with (left := encBits) (isPPTOn_sampleList.preprocess (by fun_prop)) ?_ + exact hdecode.isPPTOn /-- The tape budget covers every well-formed public observation at this dimension. -/ theorem observation_coinBudget_le (c d n : ℕ) (image : List Bool) @@ -283,7 +313,7 @@ theorem eval_wordInversionGame {n imageLength : ℕ} {Image : Type*} [DecidableE Function.comp_def, hf, beq_eq_decide, encodeImage.injective.eq_iff] /-- Holenstein's entropy-versus-prediction bound for the executable word games. Every sampled -bit and decoder query is included in the inverter certified by `isPPT_wordInverter`. -/ +bit and decoder query is included in the inverter certified by `isPPTOn_wordInverter`. -/ theorem word_prediction_entropy_le {n imageLength : ℕ} {Image : Type*} [Finite Image] (f : List Bool → List Bool) (finiteFunction : BitString n → Image) diff --git a/ComplexityTests/Crypto/Nonuniform.lean b/ComplexityTests/Crypto/Nonuniform.lean index 63ee3c5ed5..560e43c4c9 100644 --- a/ComplexityTests/Crypto/Nonuniform.lean +++ b/ComplexityTests/Crypto/Nonuniform.lean @@ -6,6 +6,7 @@ Authors: Samuel Schlesinger import Complexity.Crypto.Computational.Nonuniform.ZeroKnowledge import Complexity.Crypto.Computational.Stretch +import Complexity.Crypto.Computational.Pseudoentropy.OneWay /-! 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 @@ -21,6 +22,12 @@ open Cslib Cslib.Crypto example (word : List Bool) : ¬ NonuniformOneWay (fun _ => word) := fun h => not_oneWay_const word h.toOneWay +/-- Inverting a constant function is not hard even with empty advice: by +`oneWay_iff_inversionHardWithAdvice_nil` that would make it uniformly one-way. -/ +example (word : List Bool) : ¬ InversionHardWithAdvice (fun _ => word) (fun _ => []) := + fun h => not_oneWay_const word (oneWay_iff_inversionHardWithAdvice_nil.mpr + ⟨Turing.MultiTapeTM.ComputableInPolyTime.const word, h⟩) + /-- The nonuniform indistinguishability relation holds between equal ensembles. -/ example : NonuniformlyIndistinguishable (fun n => BitString.uniformList n) (fun n => BitString.uniformList n) := @@ -69,4 +76,12 @@ example {generator : List Bool → List Bool} (h : NonuniformPRG generator (fun (h.amplify (fun n => 3 * n + 1) (by fun_prop) (fun n => by omega)) |>.exists_auxiliaryInputZeroKnowledge_of_mem_NP (fun _ => le_rfl) hA +/-- A pair with a prediction gap against predictors given empty advice has the uniform gap, so the +fair-coin bound of `HasGap` applies to it. -/ +example {pair : Pseudoentropy.SamplablePair} {gap : ℕ → ℝ} + (h : pair.HasGapWithAdvice gap (fun _ => [])) : + ∀ᶠ n in Filter.atTop, Probability.PMF.conditionalEntropy (pair.joint n) + gap n ≤ 1 := + (Pseudoentropy.SamplablePair.hasGap_iff_hasGapWithAdvice_nil.mpr + h).eventually_entropy_add_gap_le_one + end ComplexityTests.Crypto.Nonuniform