From 0a6b3c5caae061bf0b4ffe161cc86d8bb27cb0a3 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 16:42:43 +0000 Subject: [PATCH 1/5] feat(Crypto): nonuniform one-way functions and PRGs with the GMW advice bridge Add NonuniformlyIndistinguishable, NonuniformOneWay and NonuniformPRG (uniform strict PPT adversaries with polynomially bounded advice), their uniform projections, encoded-advice bridges via the new IsPPTOn.exists_extension, and NonuniformPRG.advicePRG discharging the GMW.AdvicePRG premise of the auxiliary-input GMW theorem. Link #2316 from ROADMAP landmark 1. Milestone M1 of #2316. AI-assisted: worker-jetski-3ceb65c9 (Jetski/Gemini). --- Complexity.lean | 3 + .../Probabilistic/PPT/Extension.lean | 64 +++++ .../Computational/Nonuniform/Basic.lean | 258 ++++++++++++++++++ .../Nonuniform/ZeroKnowledge.lean | 87 ++++++ ComplexityTests/Crypto/Nonuniform.lean | 57 ++++ ROADMAP.md | 5 +- 6 files changed, 472 insertions(+), 2 deletions(-) create mode 100644 Complexity/Computability/Probabilistic/PPT/Extension.lean create mode 100644 Complexity/Crypto/Computational/Nonuniform/Basic.lean create mode 100644 Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean create mode 100644 ComplexityTests/Crypto/Nonuniform.lean diff --git a/Complexity.lean b/Complexity.lean index c7067b308e..4784dba1b2 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2434,6 +2434,7 @@ public import Complexity.Computability.Probabilistic.PPT public import Complexity.Computability.Probabilistic.PPT.Capture public import Complexity.Computability.Probabilistic.PPT.Clock public import Complexity.Computability.Probabilistic.PPT.Composition +public import Complexity.Computability.Probabilistic.PPT.Extension public import Complexity.Computability.Probabilistic.Parameter public import Complexity.Computability.Probabilistic.Presample public import Complexity.Computability.Probabilistic.QueryBounds @@ -2799,6 +2800,8 @@ public import Complexity.Crypto.Computational.MerkleTree.Binding public import Complexity.Crypto.Computational.NaorReingold public import Complexity.Crypto.Computational.NaorReingold.PRF public import Complexity.Crypto.Computational.NaorReingold.Security +public import Complexity.Crypto.Computational.Nonuniform.Basic +public import Complexity.Crypto.Computational.Nonuniform.ZeroKnowledge public import Complexity.Crypto.Computational.OneWay public import Complexity.Crypto.Computational.OneWay.Amplification public import Complexity.Crypto.Computational.OneWay.BPP diff --git a/Complexity/Computability/Probabilistic/PPT/Extension.lean b/Complexity/Computability/Probabilistic/PPT/Extension.lean new file mode 100644 index 0000000000..7d531e5f28 --- /dev/null +++ b/Complexity/Computability/Probabilistic/PPT/Extension.lean @@ -0,0 +1,64 @@ +/- +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.Computability.Probabilistic.PPT.Composition +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Plain + +/-! +# Extending efficient programs to all words + +An `IsPPTOn input output program` certificate fixes a machine on encoded inputs only. Running the +same machine, with the same clock, on an arbitrary word gives a program on all words that agrees +with `program` on every codeword `input a`. Its outputs on other words need not be codewords, so +a polynomial-time left inverse of the output encoding turns them into typed results. + +This is the step that lets a reduction receive data it cannot decode efficiently, such as an +advice word holding an `input`-encoded value for an arbitrary encoding: the reduction passes the +word to the extension, which reads it exactly as the original machine would. + +## Main results + +* `Cslib.Probability.IsPPTOn.exists_extension`: a uniform PPT program on all words agreeing with + the original program on its codewords. +-/ + +@[expose] public section + +namespace Cslib.Probability + +open Turing.MultiTapeTM + +variable {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} + +/-- **Extension to all words.** A uniform strict PPT program on encoded inputs extends to a +uniform strict PPT program on all words that agrees with it on every codeword, given a +polynomial-time left inverse `decode` of the output encoding. The extension runs the original +machine; on words outside the range of `input` its results are whatever `decode` makes of the +machine's output. -/ +theorem IsPPTOn.exists_extension {program : α → ProbComp β} (h : IsPPTOn input output program) + {decode : List Bool → β} (hdecode : ComputableInPolyTime decode encBits output) + (hleft : ∀ b, decode (output b) = b) : + ∃ extension : List Bool → ProbComp β, IsPPTOn encBits output extension ∧ + ∀ a, ProbComp.eval (extension (input a)) = ProbComp.eval (program a) := by + obtain ⟨k, State, hfinite, machine, c, d, hmachine⟩ := isPPTOn_iff_encoded.mp h + have hrun : IsPPTOn encBits encBits + (fun word => machine.runClosed (c * (word.length + 1) ^ d) word) := + ⟨k, State, hfinite, machine, c, d, fun word => by + simp only [encBits, Function.Embedding.coe_refl, PMF.map_id, id]⟩ + refine ⟨fun word => decode <$> machine.runClosed (c * (word.length + 1) ^ d) word, + hrun.map hdecode, fun a => ?_⟩ + have hencoded := hmachine a + simp only [encBits, Function.Embedding.coe_refl, PMF.map_id] at hencoded + rw [ProbComp.eval_map, ← hencoded, ProbComp.eval_map, PMF.map_comp] + conv_rhs => rw [← PMF.map_id (ProbComp.eval (program a))] + congr 1 + funext b + exact hleft b + +end Cslib.Probability diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean new file mode 100644 index 0000000000..d2b5e71474 --- /dev/null +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -0,0 +1,258 @@ +/- +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.Crypto.Computational.OneWay +public import Complexity.Crypto.Computational.PseudorandomGenerator +import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List +import Complexity.Computability.Probabilistic.PPT.Extension +import Complexity.Crypto.Negligible.Basic +import Complexity.Probability.BitString +import Complexity.Tactic.PPT + +/-! +# Security against adversaries with advice + +Nonuniform security lets every adversary read, besides the unary parameter `n` and its +challenge, an advice word `advice n` from an arbitrary family whose lengths are polynomially +bounded. The adversary itself is still one uniform strict PPT program, clocked on the whole +input, including the advice. This is the usual "PPT with polynomial advice" adversary class: the +family need not be computable, so it can hard-wire information about every parameter separately. + +`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. Conversely, an advice word may carry a value of any type under +any encoding (`NonuniformlyIndistinguishable.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. + +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.NonuniformOneWay`: one-wayness against inverters given polynomially bounded + advice. +* `Cslib.Crypto.NonuniformPRG`: a stretching generator whose output is nonuniformly + indistinguishable from uniform. + +## Main results + +* `Cslib.Crypto.NonuniformlyIndistinguishable.refl`, + `Cslib.Crypto.NonuniformlyIndistinguishable.symm`, + `Cslib.Crypto.NonuniformlyIndistinguishable.trans`: an equivalence relation on ensembles. +* `Cslib.Crypto.NonuniformlyIndistinguishable.computationallyIndistinguishable`, + `Cslib.Crypto.NonuniformOneWay.toOneWay`, `Cslib.Crypto.NonuniformPRG.toPRG`: nonuniform + security implies uniform security. +* `Cslib.Crypto.NonuniformlyIndistinguishable.negligible_encoded`, + `Cslib.Crypto.NonuniformOneWay.inversion_negligible_encoded`: advice of any encoded type. +* `Cslib.Crypto.not_nonuniformlyIndistinguishable_pure_uniformList`: advice distinguishes every + fixed family of words from uniform words, whether or not the family is computable. + +## References + +* [O. Goldreich, *Foundations of Cryptography, Volume 1*][Goldreich2001], Sections 2.2 and 3.2. +-/ + +@[expose] public section + +namespace Cslib.Crypto + +open Probability Turing.MultiTapeTM +open scoped NNReal ENNReal + +/-- A uniform adversary is an advice adversary that ignores its advice. -/ +private theorem isPPTOn_dropAdvice {β : Type} {output : β ↪ List Bool} + {adversary : ℕ → List Bool → ProbComp β} (h : IsPPT output adversary) : + IsPPTOn (encPair (encPair encUnary encBits) encBits) output + (fun input : (ℕ × List Bool) × List Bool => adversary input.1.1 input.2) := + 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. -/ +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) + +/-- Every ensemble is nonuniformly indistinguishable from itself. -/ +theorem NonuniformlyIndistinguishable.refl (X : ℕ → PMF (List Bool)) : + NonuniformlyIndistinguishable X X := fun _ _ => Game.Indistinguishable.refl _ _ + +/-- Nonuniform indistinguishability is symmetric. -/ +theorem NonuniformlyIndistinguishable.symm {X Y : ℕ → PMF (List Bool)} + (h : NonuniformlyIndistinguishable X Y) : NonuniformlyIndistinguishable Y X := + fun advice hadvice => (h advice hadvice).symm + +/-- Nonuniform indistinguishability composes through an intermediate ensemble. -/ +theorem NonuniformlyIndistinguishable.trans {X Y Z : ℕ → PMF (List Bool)} + (hXY : NonuniformlyIndistinguishable X Y) (hYZ : NonuniformlyIndistinguishable Y Z) : + NonuniformlyIndistinguishable X Z := + fun advice hadvice => (hXY advice hadvice).trans (hYZ advice hadvice) + +/-- Nonuniform indistinguishability implies uniform indistinguishability: a uniform test ignores +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} + {test : (ℕ × γ) × List Bool → ProbComp Bool} + (htest : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBool test) + {advice : ℕ → γ} (hadvice : PolynomiallyBounded (fun n => (encAdvice (advice n)).length)) : + 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 + obtain ⟨extension, hextension, heq⟩ := + htest.exists_extension (ComputableInPolyTime.headD false) (fun _ => rfl) + have hword : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBool + (fun input => extension (encPair (encPair encUnary encBits) encBits input)) := + hextension.preprocess (ComputableInPolyTime.of_eq fun _ => rfl) + have hkey (n : ℕ) (word : List Bool) : + 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 + +/-- **Advice distinguishes fixed words from uniform words.** For every family of words with +polynomially bounded lengths, computable or not, the point masses at those words are not +nonuniformly indistinguishable from uniform words of any eventually positive lengths: the test +compares its sample with its advice. Uniform tests cannot do this for every family, so the advice +in `NonuniformlyIndistinguishable` is not vacuous. -/ +theorem not_nonuniformlyIndistinguishable_pure_uniformList (target : ℕ → List Bool) + (htarget : PolynomiallyBounded (fun n => (target n).length)) {length : ℕ → ℕ} + (hlength : ∀ᶠ n in Filter.atTop, 1 ≤ length n) : + ¬ NonuniformlyIndistinguishable (fun n => PMF.pure (target n)) + (fun n => BitString.uniformList (length n)) := by + intro h + have hcompare : ComputableInPolyTime + (fun input : (ℕ × List Bool) × List Bool => input.2 == input.1.2) + (encPair (encPair encUnary encBits) encBits) encBool := by fun_prop + have hneg := h target htarget (fun input => pure (input.2 == input.1.2)) hcompare.isPPTOn + refine not_negligible_const (c := 1 / 2) (by norm_num) (negligible_of_eventually_le hneg ?_) + filter_upwards [hlength] with n hn + have hreal : distinguishingGame (PMF.pure (target n)) + (fun word => pure (word == target n)) = PMF.pure true := by + simp [distinguishingGame] + have hideal : distinguishingGame (BitString.uniformList (length n)) + (fun word => pure (word == target n)) true = + BitString.uniformList (length n) (target n) := by + simp [distinguishingGame] + have hle : (Game.succProbability (distinguishingGame (BitString.uniformList (length n)) + (fun word => pure (word == target n))) : ℝ) ≤ 1 / 2 := by + rw [Game.coe_succProbability, hideal] + have hbound := BitString.uniformList_apply_le (length n) (target n) + have hpow : (1 : ℝ≥0∞) / 2 ^ length n ≤ 1 / 2 := by + gcongr + exact le_self_pow₀ (by norm_num) (by omega) + have := ENNReal.toReal_mono (by norm_num) (hbound.trans hpow) + simpa using this + rw [← NNReal.coe_le_coe, Game.coe_advantage, hreal] + have hone : (Game.succProbability (PMF.pure true) : ℝ) = 1 := by simp + rw [hone] + calc ((1 / 2 : ℝ≥0) : ℝ) = 1 - 1 / 2 := by norm_num + _ ≤ 1 - _ := by linarith + _ ≤ |1 - _| := le_abs_self _ + +/-- 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)) : + 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 + +/-- **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} + {adversary : (ℕ × γ) × List Bool → ProbComp (List Bool)} + (hPPT : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBits adversary) + {advice : ℕ → γ} (hadvice : PolynomiallyBounded (fun n => (encAdvice (advice n)).length)) : + Negligible (fun n => Game.succProbability (ProbComp.eval + (inversionGame f (fun n image => adversary ((n, advice n), image)) n))) := by + obtain ⟨extension, hextension, heq⟩ := + hPPT.exists_extension (decode := id) (ComputableInPolyTime.of_eq fun _ => rfl) (fun _ => rfl) + have hword : IsPPTOn (encPair (encPair encUnary encBits) encBits) encBits + (fun input => extension (encPair (encPair encUnary encBits) encBits input)) := + hextension.preprocess (ComputableInPolyTime.of_eq fun _ => rfl) + have hkey (n : ℕ) (image : List Bool) : + ProbComp.eval (extension (encPair (encPair encUnary encBits) encBits + ((n, encAdvice (advice n)), image))) = ProbComp.eval (adversary ((n, advice n), image)) := + heq ((n, advice n), image) + have hgame (n : ℕ) : + ProbComp.eval (inversionGame f (fun n image => extension + (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 + +/-- 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 + +/-- 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 +nonuniformly indistinguishable from a uniform word of the output length. -/ +structure NonuniformPRG (generator : List Bool → List Bool) (length : ℕ → ℕ) : Prop where + /-- One deterministic polynomial-time machine evaluates the generator. -/ + polyTime : ComputableInPolyTime generator encBits encBits + /-- The output length depends only on the seed length. -/ + length_eq : ∀ word, (generator word).length = length word.length + /-- Every seed length is strictly expanded. -/ + stretch : ∀ n, n < length n + /-- Generated words are indistinguishable from uniform words with polynomially bounded advice. -/ + secure : NonuniformlyIndistinguishable (generatorEnsemble generator) + (fun n => BitString.uniformList (length n)) + +/-- A nonuniform pseudorandom generator is a uniform pseudorandom generator. -/ +theorem NonuniformPRG.toPRG {generator : List Bool → List Bool} {length : ℕ → ℕ} + (h : NonuniformPRG generator length) : PseudorandomGenerator generator length := + .of_indistinguishable h.polyTime h.length_eq h.stretch + h.secure.computationallyIndistinguishable + +end Cslib.Crypto diff --git a/Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean b/Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean new file mode 100644 index 0000000000..2475a0e152 --- /dev/null +++ b/Complexity/Crypto/Computational/Nonuniform/ZeroKnowledge.lean @@ -0,0 +1,87 @@ +/- +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.Crypto.Computational.Nonuniform.Basic +public import Complexity.Crypto.Computational.ZeroKnowledge +import Complexity.Tactic.PPT + +/-! +# Auxiliary-input zero knowledge from a nonuniform generator + +`GMW.AdvicePRG enc generator length` is the security premise of the auxiliary-input +Goldreich–Micali–Wigderson theorem +`PseudorandomGenerator.exists_auxiliaryInputZeroKnowledge_of_mem_NP`: a test reading an instance, +a witness and an auxiliary input from arbitrary polynomially bounded families cannot distinguish +the generator's output at seed length `n + 7` from uniform. A nonuniform pseudorandom generator +satisfies it: the three families form one advice value under the pair encoding, which the test +reads without decoding, and the parameter shift by `7` is polynomial-time preprocessing. + +This discharges the premise from `NonuniformPRG`. It does not derive a nonuniform generator from a +(nonuniform) one-way function; that is milestone M2 of [#2316]. + +## Main results + +* `Cslib.Crypto.NonuniformPRG.advicePRG`: a nonuniform PRG satisfies `GMW.AdvicePRG`. +* `Cslib.Crypto.NonuniformPRG.exists_auxiliaryInputZeroKnowledge_of_mem_NP`: given a nonuniform + PRG with stretch at least `3 * k + 1`, every language in `NP` has an auxiliary-input + zero-knowledge proof system. + +## References + +* [O. Goldreich, S. Micali, A. Wigderson, *Proofs that Yield Nothing but Their Validity or All + Languages in NP Have Zero-Knowledge Proof Systems*][GoldreichMicaliWigderson1991] + +[#2316]: https://github.com/cslib-community/complexitylib/issues/2316 +-/ + +@[expose] public section + +namespace Cslib.Crypto + +open Probability Complexity Turing.MultiTapeTM + +/-- A **nonuniform PRG satisfies the GMW advice premise** for every instance encoding: the +instance, witness and auxiliary-input families together are one polynomially bounded advice +family, and the test runs at parameter `n + 7` on the advice for `n`. -/ +theorem NonuniformPRG.advicePRG {generator : List Bool → List Bool} {length : ℕ → ℕ} + (h : NonuniformPRG generator length) {α : Type} (enc : α ↪ List Bool) : + GMW.AdvicePRG enc generator length := by + refine ⟨h.polyTime, h.length_eq, fun test htest a w z ha hw hz => ?_⟩ + let encAdvice := encPair enc (encPair encBits encBits) + have hshift : IsPPTOn (encPair (encPair encUnary encAdvice) encBits) encBool + (fun input : (ℕ × (α × (List Bool × List Bool))) × List Bool => + test ((input.1.1 - 7, input.1.2), input.2)) := + htest.preprocess (by fun_prop) + have hsub : PolynomiallyBounded (fun m => m - 7) := PolynomiallyBounded.id.tsub _ + have ha' := ha.comp hsub + have hw' := hw.comp hsub + have hz' := hz.comp hsub + have hadvice : PolynomiallyBounded (fun m => + (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 + 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] + +/-- **Auxiliary-input GMW zero knowledge from a nonuniform PRG.** Given a nonuniform +pseudorandom generator with stretch at least `3 * k + 1`, every language `A ∈ NP enc` has a +computational zero-knowledge interactive proof system satisfying auxiliary-input zero knowledge +(`ZeroKnowledgeProof.AuxiliaryInputZeroKnowledge`). Soundness error is the constant of +`ZeroKnowledgeProof`, not negligible. -/ +theorem NonuniformPRG.exists_auxiliaryInputZeroKnowledge_of_mem_NP + {α : Type} {enc : α ↪ List Bool} {A : Set α} + {generator : List Bool → List Bool} {length : ℕ → ℕ} + (h : NonuniformPRG generator length) (hstretch : ∀ k, 3 * k + 1 ≤ length k) + (hA : A ∈ NP enc) : + ∃ zk : ZeroKnowledgeProof enc A, zk.AuxiliaryInputZeroKnowledge := + h.toPRG.exists_auxiliaryInputZeroKnowledge_of_mem_NP hstretch (h.advicePRG enc) hA + +end Cslib.Crypto diff --git a/ComplexityTests/Crypto/Nonuniform.lean b/ComplexityTests/Crypto/Nonuniform.lean new file mode 100644 index 0000000000..49bf535575 --- /dev/null +++ b/ComplexityTests/Crypto/Nonuniform.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Crypto.Computational.Nonuniform.ZeroKnowledge + +/-! 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 +(constant functions and length-wise constant generators fail them), that the indistinguishability +notion is not trivially false, and that its advice is used: a test reading its advice separates a +fixed word from uniform words. -/ + +namespace ComplexityTests.Crypto.Nonuniform + +open Cslib Cslib.Crypto + +/-- A constant function is not nonuniformly one-way, because it is not even uniformly one-way. -/ +example (word : List Bool) : ¬ NonuniformOneWay (fun _ => word) := + fun h => not_oneWay_const word h.toOneWay + +/-- The nonuniform indistinguishability relation holds between equal ensembles. -/ +example : NonuniformlyIndistinguishable (fun n => BitString.uniformList n) + (fun n => BitString.uniformList n) := + NonuniformlyIndistinguishable.refl _ + +/-- Advice separates the all-`true` word from a uniform word of each length. -/ +example : ¬ NonuniformlyIndistinguishable (fun n => PMF.pure (List.replicate n true)) + (fun n => BitString.uniformList n) := + not_nonuniformlyIndistinguishable_pure_uniformList _ + (by simp only [List.length_replicate]; fun_prop) (Filter.eventually_ge_atTop 1) + +/-- A generator that, at each seed length, outputs one fixed word of the right length is not a +nonuniform PRG: the advice holds that word. -/ +example : ¬ NonuniformPRG (fun seed => List.replicate (seed.length + 1) false) (· + 1) := by + intro h + refine not_nonuniformlyIndistinguishable_pure_uniformList (fun n => List.replicate (n + 1) false) + (by simp only [List.length_replicate]; fun_prop) (.of_forall fun n => Nat.le_add_left 1 n) ?_ + have hensemble : + generatorEnsemble (fun seed => List.replicate (seed.length + 1) false) = + fun n => PMF.pure (List.replicate (n + 1) false) := by + funext n + rw [generatorEnsemble_postprocess (fun _ => []) (fun n _ => List.replicate (n + 1) false)] + simp only [generatorEnsemble, PMF.map_comp] + exact PMF.map_const _ _ + have hsecure := h.secure + rw [hensemble] at hsecure + exact hsecure + +/-- The nonuniform generator premise gives the GMW advice premise for CNF instances. -/ +example {generator : List Bool → List Bool} {length : ℕ → ℕ} + (h : NonuniformPRG generator length) : + GMW.AdvicePRG Complexity.encCNF generator length := + h.advicePRG _ + +end ComplexityTests.Crypto.Nonuniform diff --git a/ROADMAP.md b/ROADMAP.md index 125dfd9d75..404bbd6a1a 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -33,7 +33,7 @@ the FHE industrial context, the first-order design decisions and the repository' Priorities live in this list and in the tiers of [#897]. -1. [Goldreich–Micali–Wigderson zero knowledge in full](#cryptographic-landmarks) +1. [Goldreich–Micali–Wigderson zero knowledge in full](#cryptographic-landmarks) ([#2316]) 2. [Rompel's signature theorem](#cryptographic-landmarks) ([#1001]) 3. [Completeness of oblivious transfer](#cryptographic-landmarks) 4. [Håstad's optimal MAX-E3SAT hardness](#approximation-and-pcp) ([#886]) @@ -47,7 +47,7 @@ Priorities live in this list and in the tiers of [#897]. ### Cryptographic landmarks -- **Goldreich–Micali–Wigderson zero knowledge in full.** If one-way functions exist, every +- **Goldreich–Micali–Wigderson zero knowledge in full** ([#2316]). If one-way functions exist, every language in NP has a computational zero-knowledge proof in Goldreich's sense (Def. 4.3.10): for every `x ∈ L` and arbitrary auxiliary input `z`, against probabilistic polynomial-time verifiers. This needs a bridge between the security premise and a clock independent of an @@ -830,3 +830,4 @@ not planned, not as proved. [#2145]: https://github.com/cslib-community/complexitylib/issues/2145 [#2146]: https://github.com/cslib-community/complexitylib/issues/2146 [#2084]: https://github.com/cslib-community/complexitylib/issues/2084 +[#2316]: https://github.com/cslib-community/complexitylib/issues/2316 From 5fc122d6e2e2e606fe1f17d59d76119aa7c1d44b Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 16:51:16 +0000 Subject: [PATCH 2/5] fix(Crypto): fixed-word nonvacuity is uniform; reword advice claims Prove not_computationallyIndistinguishable_pure_uniformList with the first-bit test and derive the nonuniform version from it, rewording the advice-separation claims to nonvacuity. Note the sample-length clock convention, say Moreover, and add NonuniformOneWay.of_inversion_negligible. --- .../Computational/Nonuniform/Basic.lean | 84 +++++++++++-------- ComplexityTests/Crypto/Nonuniform.lean | 15 ++-- 2 files changed, 54 insertions(+), 45 deletions(-) diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index d2b5e71474..74ac39dd04 100644 --- a/Complexity/Crypto/Computational/Nonuniform/Basic.lean +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -27,7 +27,7 @@ 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. Conversely, an advice word may carry a value of any type under +implies its uniform counterpart. Moreover, an advice word may carry a value of any type under any encoding (`NonuniformlyIndistinguishable.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. @@ -48,13 +48,15 @@ These are definitions, not assertions that such primitives exist. * `Cslib.Crypto.NonuniformlyIndistinguishable.refl`, `Cslib.Crypto.NonuniformlyIndistinguishable.symm`, `Cslib.Crypto.NonuniformlyIndistinguishable.trans`: an equivalence relation on ensembles. +* `Cslib.Crypto.NonuniformOneWay.of_inversion_negligible`: the inversion-probability constructor. * `Cslib.Crypto.NonuniformlyIndistinguishable.computationallyIndistinguishable`, `Cslib.Crypto.NonuniformOneWay.toOneWay`, `Cslib.Crypto.NonuniformPRG.toPRG`: nonuniform security implies uniform security. * `Cslib.Crypto.NonuniformlyIndistinguishable.negligible_encoded`, `Cslib.Crypto.NonuniformOneWay.inversion_negligible_encoded`: advice of any encoded type. -* `Cslib.Crypto.not_nonuniformlyIndistinguishable_pure_uniformList`: advice distinguishes every - fixed family of words from uniform words, whether or not the family is computable. +* `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. ## References @@ -78,7 +80,9 @@ private theorem isPPTOn_dropAdvice {β : Type} {output : β ↪ List Bool} /-- 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. -/ +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. -/ def NonuniformlyIndistinguishable (X Y : ℕ → PMF (List Bool)) : Prop := ∀ advice : ℕ → List Bool, PolynomiallyBounded (fun n => (advice n).length) → Game.Indistinguishable @@ -136,45 +140,38 @@ theorem NonuniformlyIndistinguishable.negligible_encoded {X Y : ℕ → PMF (Lis simpa only [distinguishingGame, hkey] using h (fun n => encAdvice (advice n)) hadvice _ hword -/-- **Advice distinguishes fixed words from uniform words.** For every family of words with -polynomially bounded lengths, computable or not, the point masses at those words are not -nonuniformly indistinguishable from uniform words of any eventually positive lengths: the test -compares its sample with its advice. Uniform tests cannot do this for every family, so the advice -in `NonuniformlyIndistinguishable` is not vacuous. -/ -theorem not_nonuniformlyIndistinguishable_pure_uniformList (target : ℕ → List Bool) - (htarget : PolynomiallyBounded (fun n => (target n).length)) {length : ℕ → ℕ} - (hlength : ∀ᶠ n in Filter.atTop, 1 ≤ length n) : - ¬ NonuniformlyIndistinguishable (fun n => PMF.pure (target n)) +/-- **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 +coin. This needs no bound on `target`. -/ +theorem not_computationallyIndistinguishable_pure_uniformList (target : ℕ → List Bool) + {length : ℕ → ℕ} (hlength : ∀ᶠ n in Filter.atTop, 1 ≤ length n) : + ¬ ComputationallyIndistinguishable (fun n => PMF.pure (target n)) (fun n => BitString.uniformList (length n)) := by intro h - have hcompare : ComputableInPolyTime - (fun input : (ℕ × List Bool) × List Bool => input.2 == input.1.2) - (encPair (encPair encUnary encBits) encBits) encBool := by fun_prop - have hneg := h target htarget (fun input => pure (input.2 == input.1.2)) hcompare.isPPTOn + have hfirst : IsPPT encBool (fun _ word => pure (word.headD false)) := + (ComputableTidilyInPolyTime.headD false).isPPT + have hneg := h _ hfirst refine not_negligible_const (c := 1 / 2) (by norm_num) (negligible_of_eventually_le hneg ?_) filter_upwards [hlength] with n hn - have hreal : distinguishingGame (PMF.pure (target n)) - (fun word => pure (word == target n)) = PMF.pure true := by + obtain ⟨m, hm⟩ : ∃ m, length n = m + 1 := ⟨length n - 1, by omega⟩ + have hreal : distinguishingGame (PMF.pure (target n)) (fun word => pure (word.headD false)) = + PMF.pure ((target n).headD false) := by simp [distinguishingGame] have hideal : distinguishingGame (BitString.uniformList (length n)) - (fun word => pure (word == target n)) true = - BitString.uniformList (length n) (target n) := by - simp [distinguishingGame] - have hle : (Game.succProbability (distinguishingGame (BitString.uniformList (length n)) - (fun word => pure (word == target n))) : ℝ) ≤ 1 / 2 := by - rw [Game.coe_succProbability, hideal] - have hbound := BitString.uniformList_apply_le (length n) (target n) - have hpow : (1 : ℝ≥0∞) / 2 ^ length n ≤ 1 / 2 := by - gcongr - exact le_self_pow₀ (by norm_num) (by omega) - have := ENNReal.toReal_mono (by norm_num) (hbound.trans hpow) - simpa using this - rw [← NNReal.coe_le_coe, Game.coe_advantage, hreal] - have hone : (Game.succProbability (PMF.pure true) : ℝ) = 1 := by simp - rw [hone] - calc ((1 / 2 : ℝ≥0) : ℝ) = 1 - 1 / 2 := by norm_num - _ ≤ 1 - _ := by linarith - _ ≤ |1 - _| := le_abs_self _ + (fun word => pure (word.headD false)) = PMF.uniformOfFintype Bool := by + rw [hm, BitString.uniformList_succ] + simp [distinguishingGame, PMF.bind_map, Function.comp_def] + rw [← NNReal.coe_le_coe, Game.coe_advantage, hreal, hideal] + cases (target n).headD false <;> norm_num [Game.succProbability, ENNReal.toNNReal_ofNat] + +/-- Nonuniform indistinguishability is not trivially true: fixed words are not nonuniformly +indistinguishable from uniform words (`not_computationallyIndistinguishable_pure_uniformList`). -/ +theorem not_nonuniformlyIndistinguishable_pure_uniformList (target : ℕ → List Bool) + {length : ℕ → ℕ} (hlength : ∀ᶠ n in Filter.atTop, 1 ≤ length n) : + ¬ NonuniformlyIndistinguishable (fun n => PMF.pure (target n)) + (fun n => BitString.uniformList (length n)) := fun h => + 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 @@ -200,6 +197,19 @@ theorem NonuniformOneWay.inversion_negligible {f : List Bool → List Bool} (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 +/-- 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 := 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. -/ diff --git a/ComplexityTests/Crypto/Nonuniform.lean b/ComplexityTests/Crypto/Nonuniform.lean index 49bf535575..9fb3cbd381 100644 --- a/ComplexityTests/Crypto/Nonuniform.lean +++ b/ComplexityTests/Crypto/Nonuniform.lean @@ -8,9 +8,9 @@ import Complexity.Crypto.Computational.Nonuniform.ZeroKnowledge /-! 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 -(constant functions and length-wise constant generators fail them), that the indistinguishability -notion is not trivially false, and that its advice is used: a test reading its advice separates a -fixed word from uniform words. -/ +(constant functions, fixed words and length-wise constant generators fail them) and that the +indistinguishability notion is not trivially false. They do not separate the nonuniform notions +from the uniform ones. -/ namespace ComplexityTests.Crypto.Nonuniform @@ -25,18 +25,17 @@ example : NonuniformlyIndistinguishable (fun n => BitString.uniformList n) (fun n => BitString.uniformList n) := NonuniformlyIndistinguishable.refl _ -/-- Advice separates the all-`true` word from a uniform word of each length. -/ +/-- The all-`true` words are distinguishable from uniform words of each positive length. -/ example : ¬ NonuniformlyIndistinguishable (fun n => PMF.pure (List.replicate n true)) (fun n => BitString.uniformList n) := - not_nonuniformlyIndistinguishable_pure_uniformList _ - (by simp only [List.length_replicate]; fun_prop) (Filter.eventually_ge_atTop 1) + not_nonuniformlyIndistinguishable_pure_uniformList _ (Filter.eventually_ge_atTop 1) /-- A generator that, at each seed length, outputs one fixed word of the right length is not a -nonuniform PRG: the advice holds that word. -/ +nonuniform PRG (nor a uniform one): its output's first bit is constant. -/ example : ¬ NonuniformPRG (fun seed => List.replicate (seed.length + 1) false) (· + 1) := by intro h refine not_nonuniformlyIndistinguishable_pure_uniformList (fun n => List.replicate (n + 1) false) - (by simp only [List.length_replicate]; fun_prop) (.of_forall fun n => Nat.le_add_left 1 n) ?_ + (.of_forall fun n => Nat.le_add_left 1 n) ?_ have hensemble : generatorEnsemble (fun seed => List.replicate (seed.length + 1) false) = fun n => PMF.pure (List.replicate (n + 1) false) := by From 1d9544119ec0d705ffeba2711387efc1f0fc0f1e Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 16:51:47 +0000 Subject: [PATCH 3/5] refactor(Crypto): plain certificate for the first-bit test --- Complexity/Crypto/Computational/Nonuniform/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index 74ac39dd04..42e1b77cd4 100644 --- a/Complexity/Crypto/Computational/Nonuniform/Basic.lean +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -149,7 +149,7 @@ theorem not_computationallyIndistinguishable_pure_uniformList (target : ℕ → (fun n => BitString.uniformList (length n)) := by intro h have hfirst : IsPPT encBool (fun _ word => pure (word.headD false)) := - (ComputableTidilyInPolyTime.headD false).isPPT + ((ComputableInPolyTime.headD false).comp (ComputableInPolyTime.snd encUnary encBits)).isPPTOn have hneg := h _ hfirst refine not_negligible_const (c := 1 / 2) (by norm_num) (negligible_of_eventually_le hneg ?_) filter_upwards [hlength] with n hn From 569d242225b05f394b410471935f5054a8631480 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 16:52:15 +0000 Subject: [PATCH 4/5] wip: relativize stretch to fixed advice --- .../Computational/Nonuniform/Basic.lean | 101 ++++++++---- .../Nonuniform/ZeroKnowledge.lean | 2 +- Complexity/Crypto/Computational/Stretch.lean | 145 ++++++++++++++---- 3 files changed, 185 insertions(+), 63 deletions(-) diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index d2b5e71474..413ab0ccf8 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. Conversely, 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. Conversely, 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 @@ -51,7 +55,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_nonuniformlyIndistinguishable_pure_uniformList`: advice distinguishes every fixed family of words from uniform words, whether or not the family is computable. @@ -76,16 +83,56 @@ 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. -/ +/-- 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 test's clock is polynomial in the length of its whole input. 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)) : @@ -106,21 +153,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 + ComputationallyIndistinguishable X Y := + computationallyIndistinguishable_iff_indistinguishableWithAdvice_nil.mpr + (h _ (PolynomiallyBounded.const 0)) -/-- **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} +/-- **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 @@ -133,8 +179,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 /-- **Advice distinguishes fixed words from uniform words.** For every family of words with polynomially bounded lengths, computable or not, the point masses at those words are not 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 c1065b21cb..fac23b0878 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 @@ -348,25 +355,26 @@ 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 input => generator input.1.1 input.1.2 input.2) - (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 input => adversary input.1.1 input.1.2 input.2) → + (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 input => adversary input.1.1 input.1.2 input.2) → + ∀ 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 @@ -377,14 +385,14 @@ theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → Lis 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) + let reduction := fun n context => + test (generator n context) (seedBits n) (count n) (adversary n context) 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 + (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 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)) @@ -392,21 +400,43 @@ theorem indexed_indistinguishable {generator : ℕ → ℕ → List Bool → Lis have h := (hsecure reduction hreduce).polynomiallyBounded_mul (loss_polynomial (.of_tidy 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 +453,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 seed := 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 +505,38 @@ 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 + simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] at htarget + have hcount : ComputableTidilyInPolyTime (fun n => target n - n) encUnary encUnary := by polytime + have h := PRGStretch.nonuniformPRG hgenerator (.of_tidy 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 + simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] at htarget + have hpoly := hgenerator.polyTime.tidy + refine ⟨.of_tidy (by polytime), 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 polytime) + simpa only [← generatorEnsemble_postprocess generator (fun n word => word.take (target n)), + uniformList_take (hle _)] using h + end Cslib.Crypto From 664e905a1c58608878d3eb48255dacf4e3a65623 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 17:03:34 +0000 Subject: [PATCH 5/5] refactor(Crypto): drop unused PRGStretch.isPPT_reduction; document unbounded advice --- .../Computational/Nonuniform/Basic.lean | 3 ++- Complexity/Crypto/Computational/Stretch.lean | 20 ------------------- 2 files changed, 2 insertions(+), 21 deletions(-) diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index 71fbe1ac5d..5da5039116 100644 --- a/Complexity/Crypto/Computational/Nonuniform/Basic.lean +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -87,7 +87,8 @@ private theorem isPPTOn_dropAdvice {β : Type} {output : β ↪ List Bool} /-- 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 test's clock is polynomial in the length of its whole input, including the sample, as for +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 diff --git a/Complexity/Crypto/Computational/Stretch.lean b/Complexity/Crypto/Computational/Stretch.lean index 8368c8c04a..5ad48945d5 100644 --- a/Complexity/Crypto/Computational/Stretch.lean +++ b/Complexity/Crypto/Computational/Stretch.lean @@ -190,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)