From 0a6b3c5caae061bf0b4ffe161cc86d8bb27cb0a3 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 16:42:43 +0000 Subject: [PATCH 01/11] 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 02/11] 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 03/11] 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 04/11] 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 05/11] 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) From c930950f9126efd4d4196568ff9b5acd90c80c43 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 17:03:55 +0000 Subject: [PATCH 06/11] feat(Crypto): relativize one-wayness to fixed advice and normalize nonuniform OWFs --- .../Computational/Nonuniform/Basic.lean | 144 ++++++++++++------ .../Computational/OneWay/Normalize.lean | 81 +++++++--- ComplexityTests/Crypto/Nonuniform.lean | 6 + 3 files changed, 158 insertions(+), 73 deletions(-) diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index 71fbe1ac5d..85ad02c3cc 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. @@ -218,51 +223,44 @@ 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. 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⟩ := @@ -279,16 +277,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..61319b1721 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 @@ -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/ComplexityTests/Crypto/Nonuniform.lean b/ComplexityTests/Crypto/Nonuniform.lean index 63ee3c5ed5..f818b494b6 100644 --- a/ComplexityTests/Crypto/Nonuniform.lean +++ b/ComplexityTests/Crypto/Nonuniform.lean @@ -21,6 +21,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) := From 9c38a8f8329a30d3ee6dd6cd7e1b92e135b84403 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 17:26:39 +0000 Subject: [PATCH 07/11] doc(Crypto): unbounded advice in InversionHardWithAdvice; plain-certificate note in Normalize --- Complexity/Crypto/Computational/Nonuniform/Basic.lean | 5 +++-- Complexity/Crypto/Computational/OneWay/Normalize.lean | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Complexity/Crypto/Computational/Nonuniform/Basic.lean b/Complexity/Crypto/Computational/Nonuniform/Basic.lean index 3cde9e7f9c..995515ac49 100644 --- a/Complexity/Crypto/Computational/Nonuniform/Basic.lean +++ b/Complexity/Crypto/Computational/Nonuniform/Basic.lean @@ -226,8 +226,9 @@ theorem not_nonuniformlyIndistinguishable_pure_uniformList (target : ℕ → Lis /-- **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. With empty advice this is the security condition of -`OneWay` (`oneWay_iff_inversionHardWithAdvice_nil`). -/ +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 => diff --git a/Complexity/Crypto/Computational/OneWay/Normalize.lean b/Complexity/Crypto/Computational/OneWay/Normalize.lean index 61319b1721..993086580d 100644 --- a/Complexity/Crypto/Computational/OneWay/Normalize.lean +++ b/Complexity/Crypto/Computational/OneWay/Normalize.lean @@ -46,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 From 1cbc241aac6c5afee424b9fa5c8bc3ebc7596621 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 17:36:18 +0000 Subject: [PATCH 08/11] refactor(Probability): plain certificates from the saved-coin evaluators --- .../Classes/Promise/Probabilistic.lean | 4 +- .../Classes/Promise/Randomized.lean | 2 +- .../Computability/Probabilistic/CoinTape.lean | 47 +++++++++++-------- .../Computability/Probabilistic/Repeat.lean | 2 +- .../Computability/Probabilistic/Traverse.lean | 2 +- .../GoldreichLevin/WordReduction.lean | 16 ++----- .../Computational/Hybrid/SavedPrediction.lean | 2 +- .../IndexedSignature/Seeded.lean | 4 +- .../Computational/OneWay/Amplification.lean | 2 +- .../Computational/OneWay/CondEPPRG.lean | 3 +- .../Computational/OneWay/LiuPassConverse.lean | 2 +- .../Crypto/Computational/OneWay/Weak.lean | 2 +- .../Computational/OneWayToSignature.lean | 4 +- .../Computational/Pseudoentropy/OneWay.lean | 2 +- .../Computational/Pseudoentropy/Seed.lean | 2 +- ComplexityTests/SeededEvaluator.lean | 6 +-- .../CryptographyBridge.lean | 2 +- 17 files changed, 54 insertions(+), 50 deletions(-) diff --git a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean index 197776d463..913c1f0cde 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Probabilistic.lean @@ -171,7 +171,7 @@ theorem mem_PromiseBPP_iff_exists_isPPTOn : Q ∈ PromiseBPP enc ↔ linarith · rintro ⟨M, hM, hyes, hno⟩ obtain ⟨c, d, evalM, hevalM, hlaw⟩ := hM.exists_seeded_evaluator - refine ⟨Polynomial.C c * (Polynomial.X + 1) ^ d, fun x => evalM x.1 x.2, .of_tidy hevalM, + refine ⟨Polynomial.C c * (Polynomial.X + 1) ^ d, fun x => evalM x.1 x.2, hevalM, fun a => ⟨fun ha => ?_, fun ha => ?_⟩⟩ · have hp : (Polynomial.C c * (Polynomial.X + 1) ^ d).eval (enc a).length = c * ((enc a).length + 1) ^ d := by simp @@ -229,7 +229,7 @@ theorem mem_PromiseRP_iff_exists_isPPTOn : Q ∈ PromiseRP enc ↔ exact Bool.noConfusion hVw · rintro ⟨M, hM, hyes, hno⟩ obtain ⟨c, d, evalM, hevalM, hsupp, hlaw⟩ := hM.exists_total_seeded_evaluator - refine ⟨Polynomial.C c * (Polynomial.X + 1) ^ d, fun x => evalM x.1 x.2, .of_tidy hevalM, + refine ⟨Polynomial.C c * (Polynomial.X + 1) ^ d, fun x => evalM x.1 x.2, hevalM, fun a => ⟨fun ha => ?_, fun ha r => ?_⟩⟩ · have hp : (Polynomial.C c * (Polynomial.X + 1) ^ d).eval (enc a).length = c * ((enc a).length + 1) ^ d := by simp diff --git a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean index 39ac9bcd65..7da25bbbf6 100644 --- a/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean +++ b/Complexity/Computability/Complexity/Classes/Promise/Randomized.lean @@ -224,7 +224,7 @@ theorem rpReducible_iff_exists_seeded : constructor · rintro ⟨R, hR, hyes, hno⟩ obtain ⟨c, d, evalR, hevalR, hsupp, hlaw⟩ := hR.exists_total_seeded_evaluator - refine ⟨Polynomial.C c * (Polynomial.X + 1) ^ d, fun x => evalR x.1 x.2, .of_tidy hevalR, + refine ⟨Polynomial.C c * (Polynomial.X + 1) ^ d, fun x => evalR x.1 x.2, hevalR, fun a ha r => hyes a ha _ (hsupp a (List.ofFn r)), fun a ha => ?_⟩ have hp : (Polynomial.C c * (Polynomial.X + 1) ^ d).eval (encA a).length = c * ((encA a).length + 1) ^ d := by simp diff --git a/Complexity/Computability/Probabilistic/CoinTape.lean b/Complexity/Computability/Probabilistic/CoinTape.lean index ecc6b7f157..cfe99b9860 100644 --- a/Complexity/Computability/Probabilistic/CoinTape.lean +++ b/Complexity/Computability/Probabilistic/CoinTape.lean @@ -41,7 +41,7 @@ assumed: supported output words have unique preimages under the declared encodin Adapted from Computability/Probabilistic/CoinTape.lean on the cslib `crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203ccd8`, using the common machine, standard pair encoding and -tidy computability calculus. +plain polynomial-time certificates. -/ @[expose] public section @@ -53,6 +53,15 @@ open Turing Turing.MultiTapeTM variable {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} +/-- Change the output encoding along an equality of encoded values: certificates speak only about +encoded words. -/ +private theorem computableInPolyTime_of_enc_eq {γ δ : Type} {encIn : γ ↪ List Bool} + {encOut : β ↪ List Bool} {encMid : δ ↪ List Bool} {f : γ → β} {g : γ → δ} + (hg : ComputableInPolyTime g encIn encMid) (h : ∀ a, encOut (f a) = encMid (g a)) : + ComputableInPolyTime f encIn encOut := by + obtain ⟨t, s, ht, hs, k, State, hfinite, tm, htm⟩ := hg + exact ⟨t, s, ht, hs, k, State, hfinite, tm, fun a => by rw [h a]; exact htm a⟩ + /-- One finite machine and one polynomial budget realize the whole program family from saved fair bits. Neither witness depends on the input value. -/ theorem IsPPTOn.exists_coin_machine (h : IsPPTOn input output program) : @@ -69,13 +78,13 @@ theorem IsPPTOn.exists_coin_machine (h : IsPPTOn input output program) : polynomial time. Its exact realization law applies to encoded inputs at the stated budget. -/ theorem IsPPTOn.exists_polyTime_coin_evaluator (h : IsPPTOn input output program) : ∃ (c d : ℕ) (evaluate : List Bool → List Bool → List Bool), - ComputableTidilyInPolyTime (fun p : List Bool × List Bool => evaluate p.1 p.2) + ComputableInPolyTime (fun (coins, word) => evaluate coins word) (encPair encBits encBits) encBits ∧ ∀ a, (ProbComp.eval (program a)).map output = (BitString.uniformList (c * ((input a).length + 1) ^ d)).map (fun coins => evaluate coins (input a)) := by obtain ⟨k, State, _, machine, c, d, hm⟩ := h.exists_coin_machine - exact ⟨c, d, machine.runClosedCoins, machine.computableInPolyTime_runClosedCoins.tidy, hm⟩ + exact ⟨c, d, machine.runClosedCoins, machine.computableInPolyTime_runClosedCoins, hm⟩ /-- Every typed PPT program has a total deterministic polynomial-time evaluator. Every seed produces a supported result. Short seeds are padded; longer seeds are truncated to the program's @@ -84,7 +93,7 @@ budget. Every uniform seed at least that long yields exactly the program's distr Computability is relative to the output encoding and requires no decoder for invalid words. -/ theorem IsPPTOn.exists_total_seeded_evaluator (h : IsPPTOn input output program) : ∃ (c d : ℕ) (evaluate : α → List Bool → β), - ComputableTidilyInPolyTime (fun p : α × List Bool => evaluate p.1 p.2) + ComputableInPolyTime (fun (a, coins) => evaluate a coins) (encPair input encBits) output ∧ (∀ a coins, evaluate a coins ∈ (ProbComp.eval (program a)).support) ∧ ∀ a length, c * ((input a).length + 1) ^ d ≤ length → @@ -108,20 +117,20 @@ theorem IsPPTOn.exists_total_seeded_evaluator (h : IsPPTOn input output program) have hencode (a : α) (coins : List Bool) : output (evaluate a coins) = raw (tape a coins) (input a) := (hvalid a coins).choose_spec.2 refine ⟨c, d, evaluate, ?_, fun a coins => (hvalid a coins).choose_spec.1, ?_⟩ - · have hinput : ComputableTidilyInPolyTime input input encBits := .of_eq fun _ => rfl - have hbudget : ComputableTidilyInPolyTime budget input encUnary := by + · have hinput : ComputableInPolyTime (fun a => input a) input encBits := .of_eq fun _ => rfl + have hbudget : ComputableInPolyTime budget input encUnary := by dsimp only [budget] fun_prop - have hpad : ComputableTidilyInPolyTime (fun a => List.replicate (budget a) true) - input encBits := hbudget.of_enc_eq (fun _ => rfl) - have ht : ComputableTidilyInPolyTime - (fun p : α × List Bool => (tape p.1 p.2, input p.1)) + have hpad : ComputableInPolyTime (fun a => List.replicate (budget a) true) input encBits := + computableInPolyTime_of_enc_eq hbudget fun _ => rfl + have ht : ComputableInPolyTime + (fun (a, coins) => (tape a coins, input a)) (encPair input encBits) (encPair encBits encBits) := by - have hfirst := ComputableTidilyInPolyTime.fst input encBits - have hsecond := ComputableTidilyInPolyTime.snd input encBits - exact (ComputableTidilyInPolyTime.bitsTakeWithInput + have hfirst := ComputableInPolyTime.fst input encBits + have hsecond := ComputableInPolyTime.snd input encBits + exact (ComputableInPolyTime.bitsTakeWithInput (hsecond.bitsAppend (hpad.comp hfirst)) (hbudget.comp hfirst)).prod (hinput.comp hfirst) - exact (hraw.comp ht).of_enc_eq (fun p => hencode p.1 p.2) + exact computableInPolyTime_of_enc_eq (hraw.comp ht) fun (a, coins) => hencode a coins · intro a length hbudget apply PMF.map_injective output.injective rw [hlaw, PMF.map_comp, ← BitString.uniformList_take hbudget, PMF.map_comp] @@ -137,7 +146,7 @@ theorem IsPPTOn.exists_total_seeded_evaluator (h : IsPPTOn input output program) /-- The exact-budget specialization of the total seeded evaluator. -/ theorem IsPPTOn.exists_seeded_evaluator (h : IsPPTOn input output program) : ∃ (c d : ℕ) (evaluate : α → List Bool → β), - ComputableTidilyInPolyTime (fun p : α × List Bool => evaluate p.1 p.2) + ComputableInPolyTime (fun (a, coins) => evaluate a coins) (encPair input encBits) output ∧ ∀ a, ProbComp.eval (program a) = (BitString.uniformList (c * ((input a).length + 1) ^ d)).map (evaluate a) := by @@ -148,7 +157,7 @@ theorem IsPPTOn.exists_seeded_evaluator (h : IsPPTOn input output program) : raw word evaluator trims to each input's own budget and accepts arbitrary encoded words. -/ theorem IsPPTOn.exists_padded_coin_evaluator (h : IsPPTOn input output program) : ∃ (c d : ℕ) (evaluate : List Bool → List Bool → List Bool), - ComputableTidilyInPolyTime (fun p : List Bool × List Bool => evaluate p.1 p.2) + ComputableInPolyTime (fun (coins, word) => evaluate coins word) (encPair encBits encBits) encBits ∧ ∀ a length, c * ((input a).length + 1) ^ d ≤ length → (ProbComp.eval (program a)).map output = (BitString.uniformList length).map @@ -156,8 +165,8 @@ theorem IsPPTOn.exists_padded_coin_evaluator (h : IsPPTOn input output program) obtain ⟨c, d, evaluate, hefficient, hlaw⟩ := h.exists_polyTime_coin_evaluator refine ⟨c, d, fun coins input => evaluate (coins.take (c * (input.length + 1) ^ d)) input, ?_, ?_⟩ - · exact hefficient.comp (show ComputableTidilyInPolyTime - (fun p : List Bool × List Bool => (p.1.take (c * (p.2.length + 1) ^ d), p.2)) + · exact hefficient.comp (show ComputableInPolyTime + (fun (coins, word) => (coins.take (c * (word.length + 1) ^ d), word)) (encPair encBits encBits) (encPair encBits encBits) by fun_prop) · intro a length hlength rw [hlaw, ← BitString.uniformList_take hlength, PMF.map_comp] @@ -168,7 +177,7 @@ shared tape budget may depend only on a bound on the encoded input size. -/ theorem IsPPTOn.exists_padded_bool_coin_evaluator {program : α → ProbComp Bool} (h : IsPPTOn input encBool program) : ∃ (c d : ℕ) (evaluate : List Bool → List Bool → List Bool), - ComputableTidilyInPolyTime (fun p : List Bool × List Bool => evaluate p.1 p.2) + ComputableInPolyTime (fun (coins, word) => evaluate coins word) (encPair encBits encBits) encBits ∧ ∀ a length, c * ((input a).length + 1) ^ d ≤ length → ProbComp.eval (program a) = (BitString.uniformList length).map diff --git a/Complexity/Computability/Probabilistic/Repeat.lean b/Complexity/Computability/Probabilistic/Repeat.lean index 6b994cdfd5..f70e7fd35e 100644 --- a/Complexity/Computability/Probabilistic/Repeat.lean +++ b/Complexity/Computability/Probabilistic/Repeat.lean @@ -63,7 +63,7 @@ theorem IsPPTOn.replicate {α β : Type} {input : α ↪ List Bool} {output : β (encPair input encBits) (encList encBits) := by fun_prop have heval : ComputableInPolyTime (fun p : (α × List Bool) × List Bool => evaluate p.1.1 p.2) (encPair (encPair input encBits) encBits) output := - (ComputableInPolyTime.of_tidy hevaluate).comp + hevaluate.comp (((ComputableInPolyTime.fst input encBits).comp (ComputableInPolyTime.fst _ _)).prod (ComputableInPolyTime.snd _ _)) have hmap := ComputableInPolyTime.mapWithInput (f := fun q row => evaluate q.1 row) hrows heval diff --git a/Complexity/Computability/Probabilistic/Traverse.lean b/Complexity/Computability/Probabilistic/Traverse.lean index cd9559c5c6..f7b8b76648 100644 --- a/Complexity/Computability/Probabilistic/Traverse.lean +++ b/Complexity/Computability/Probabilistic/Traverse.lean @@ -87,7 +87,7 @@ theorem IsPPTOn.mapM {α β : Type} {input : α ↪ List Bool} {output : β ↪ (encPair (encList input) encBits) (encList output) := by apply ComputableTidilyInPolyTime.mapWithInput · fun_prop - · exact hevaluate.comp (show ComputableTidilyInPolyTime + · exact hevaluate.tidy.comp (show ComputableTidilyInPolyTime (fun p : (List α × List Bool) × (α × ℕ) => (p.2.1, BitString.listRow (budget p.1.1) p.2.2 p.1.2)) (encPair (encPair (encList input) encBits) (encPair input encUnary)) diff --git a/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean b/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean index 74327e10c4..c8322c8617 100644 --- a/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean +++ b/Complexity/Crypto/Computational/GoldreichLevin/WordReduction.lean @@ -207,7 +207,7 @@ theorem negligible_parityPrediction {f : List Bool → List Bool} (hf : OneWay f apply negligible_prediction_of_negligible_inversion intro degree simpa only [eval_wordInversionGame f] using - hf.inversion_negligible _ (isPPT_wordInverter hf.polyTime (.of_tidy hefficient) c d degree) + hf.inversion_negligible _ (isPPT_wordInverter hf.polyTime hefficient c d degree) /-- One efficient typed evaluator witnesses the concrete reduction at every precision degree. When `f` is efficient, `isPPT_wordInverter` certifies each resulting inverter. -/ @@ -219,15 +219,9 @@ theorem exists_word_reduction (f : List Bool → List Bool) (adversary : Disting ∀ degree n, |Pr[parityPredictionGame f adversary n] - 1 / 2| ≤ 1 / (precision degree n : ℝ) + 8 * Pr[inversionGame f (wordInverter f evaluate c d degree) n] := by - have this : ∃ (c d : ℕ) (evaluate : (ℕ × List Bool) → List Bool → Bool), - ComputableTidilyInPolyTime (fun p : (ℕ × List Bool) × List Bool => evaluate p.1 p.2) (encPair - (encPair encUnary encBits) encBits) encBool ∧ ∀ degree n, |Pr[parityPredictionGame f - adversary n] - 1 / 2| ≤ 1 / (precision degree n : ℝ) + 8 * Pr[inversionGame f (wordInverter f - evaluate c d degree) n] := by - obtain ⟨c, d, evaluate, hefficient, hrealize⟩ := hPPT.on.exists_seeded_evaluator - exact ⟨c, d, evaluate, hefficient, fun degree n => - word_prediction_advantage_le f adversary evaluate c d - (fun n input => hrealize (n, input)) degree n⟩ - simpa only [computableInPolyTime_iff_computableTidilyInPolyTime] using this + obtain ⟨c, d, evaluate, hefficient, hrealize⟩ := hPPT.on.exists_seeded_evaluator + exact ⟨c, d, evaluate, hefficient, fun degree n => + word_prediction_advantage_le f adversary evaluate c d + (fun n input => hrealize (n, input)) degree n⟩ end Cslib.Crypto.GoldreichLevin diff --git a/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean b/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean index fa922b66ab..eec8e01264 100644 --- a/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean +++ b/Complexity/Crypto/Computational/Hybrid/SavedPrediction.lean @@ -379,7 +379,7 @@ theorem exists_evaluator {Param : Type} {input : Param ↪ List Bool} {output : sequenceTest replacement original count (test a) (observation, trial))) := by simp only [Turing.MultiTapeTM.computableInPolyTime_iff_computableTidilyInPolyTime] obtain ⟨c, d, raw, hefficient, hrealize⟩ := htest.exists_padded_bool_coin_evaluator - refine ⟨c, d, evaluate raw, (isPolyTime_evaluate (.of_tidy hefficient)).tidy, ?_⟩ + refine ⟨c, d, evaluate raw, (isPolyTime_evaluate hefficient).tidy, ?_⟩ intro a replacement original count width observation hwidth apply eval_sample output (input a) replacement original count c d width (test a) raw (fun values budget hbudget => hrealize (a, values) budget hbudget) observation hwidth diff --git a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean index 6420d41f77..6c98c3e6bf 100644 --- a/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean +++ b/Complexity/Crypto/Computational/IndexedSignature/Seeded.lean @@ -102,7 +102,7 @@ theorem exists_keyGenWith (S : IndexedSignatureScheme) : ProbComp.eval (S.keyGen n) = (BitString.uniformList length).map (keyGenWith n) := by obtain ⟨c, d, evaluate, hpoly, hsupport, hlaw⟩ := IsPPTOn.exists_total_seeded_evaluator S.keyGen_ppt - exact ⟨evaluate, fun n => c * ((encUnary n).length + 1) ^ d, .of_tidy hpoly, + exact ⟨evaluate, fun n => c * ((encUnary n).length + 1) ^ d, hpoly, computableInPolyTime_coinBudget encUnary c d, hsupport, hlaw⟩ /-- Every indexed scheme has seeded signing with a polynomial-time budget. -/ @@ -122,7 +122,7 @@ theorem exists_signWith (S : IndexedSignatureScheme) : obtain ⟨c, d, evaluate, hpoly, hsupport, hlaw⟩ := IsPPTOn.exists_total_seeded_evaluator S.sign_ppt exact ⟨evaluate, fun a => c * ((encPair encBits (encPair encUnary encBits) a).length + 1) ^ d, - .of_tidy hpoly, computableInPolyTime_coinBudget _ c d, hsupport, hlaw⟩ + hpoly, computableInPolyTime_coinBudget _ c d, hsupport, hlaw⟩ /-- The seeded algorithms of any indexed scheme, read off its strict-PPT certificates. -/ noncomputable def seeded (S : IndexedSignatureScheme) : S.Seeded := diff --git a/Complexity/Crypto/Computational/OneWay/Amplification.lean b/Complexity/Crypto/Computational/OneWay/Amplification.lean index 95f2e81b40..2777b268d4 100644 --- a/Complexity/Crypto/Computational/OneWay/Amplification.lean +++ b/Complexity/Crypto/Computational/OneWay/Amplification.lean @@ -606,7 +606,7 @@ theorem familyInversionGame_parallelCore_negligible {f : List Bool → List Bool ComputableTidilyInPolyTime.unary_mul.comp ((ht.comp hn).prod (hseedLen.comp hn)) have hfst2 := ComputableTidilyInPolyTime.fst (encPair encUnary encBits) encBits have hsnd2 := ComputableTidilyInPolyTime.snd (encPair encUnary encBits) encBits - have hrun := computableTidily_runTrials hk hw ht hseedLen hweak.polyTime.tidy hevalA + have hrun := computableTidily_runTrials hk hw ht hseedLen hweak.polyTime.tidy hevalA.tidy (hn.comp hfst2) (hsnd.comp hfst2) hsnd2 exact IsPPTOn.map_with (ComputableInPolyTime.of_tidy hsample_len).sampleList (.of_tidy hrun) have hweak_w : ∀ᶠ n in atTop, diff --git a/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean b/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean index d739fc32ce..84375210d3 100644 --- a/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean +++ b/Complexity/Crypto/Computational/OneWay/CondEPPRG.lean @@ -3363,7 +3363,8 @@ theorem OneWay.exists_condEPPRG {f : List Bool → List Bool} (hf : OneWay f) ( let D_inv := (2 * d + γ_core + 2) + 3 + (E + 1) + 2 + 2 + E * δ have hinv_ppt : IsPPT encBits (condInverter g imgLen evaluate d γ_core γ c_eval d_eval deg) := - isPPT_condInverter hg.polyTime.tidy himgLen_poly.tidy hevaluate d γ_core γ c_eval d_eval deg + isPPT_condInverter hg.polyTime.tidy himgLen_poly.tidy hevaluate.tidy d γ_core γ c_eval d_eval + deg have hinv_neg := (hg.inversion_negligible _ hinv_ppt).eventually_le_inv_polynomial (p := fun k => (k + 1) ^ D_inv) (by fun_prop) (fun k => by positivity) diff --git a/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean b/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean index 2350d63827..a100625b34 100644 --- a/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean +++ b/Complexity/Crypto/Computational/OneWay/LiuPassConverse.lean @@ -675,7 +675,7 @@ theorem weakOneWay_reindex_liuPassCore obtain ⟨cA, dA, evalA, hevalA, _, hlawA⟩ := hA.on.exists_total_seeded_evaluator let H (y : List Bool) : ProbComp ℕ := heuristicCand t evalA y <$> BitString.sampleList (coinBudget cA dA y.length) - have hH_ppt : IsPPTOn encBits encNat H := isPPTOn_heuristic ht_comp.tidy hevalA + have hH_ppt : IsPPTOn encBits encNat H := isPPTOn_heuristic ht_comp.tidy hevalA.tidy filter_upwards [hK_hard H hH_ppt] with n hn_H let B := coinBudget cA dA n let distH : PMF Bool := diff --git a/Complexity/Crypto/Computational/OneWay/Weak.lean b/Complexity/Crypto/Computational/OneWay/Weak.lean index a70caf50e2..540519a0b6 100644 --- a/Complexity/Crypto/Computational/OneWay/Weak.lean +++ b/Complexity/Crypto/Computational/OneWay/Weak.lean @@ -491,7 +491,7 @@ theorem exists_familyInverter_inversion_le {m : ℕ → ℕ} {core : ℕ → Lis Game.succProbability (ProbComp.eval (familyInversionGame m core familyAdv (GeneratorReindex.parameter m M))) := by obtain ⟨c, d, evaluate, heval, _, hlaw⟩ := hPPT.on.exists_total_seeded_evaluator - refine ⟨familyInverter m core c d evaluate, isPPT_familyInverter hm.tidy hcore.tidy heval, + refine ⟨familyInverter m core c d evaluate, isPPT_familyInverter hm.tidy hcore.tidy heval.tidy, fun {M} hM0 => ?_⟩ let n := GeneratorReindex.parameter m M have hfits : m n ≤ M := GeneratorReindex.parameter_fits hM0 diff --git a/Complexity/Crypto/Computational/OneWayToSignature.lean b/Complexity/Crypto/Computational/OneWayToSignature.lean index 7694e76513..9c94db11fb 100644 --- a/Complexity/Crypto/Computational/OneWayToSignature.lean +++ b/Complexity/Crypto/Computational/OneWayToSignature.lean @@ -146,7 +146,7 @@ theorem SignatureScheme.OneTimeEUFCMA.exists_oneWay {S : SignatureScheme} hparam_unary.comp ComputableTidilyInPolyTime.length_bits have hpk : ComputableTidilyInPolyTime (fun seed : List Bool => (evaluate (param seed.length) seed).1) encBits encBits := - (ComputableTidilyInPolyTime.fst encBits encBits).comp (heval.comp (hparam.prod .id')) + (ComputableTidilyInPolyTime.fst encBits encBits).comp (heval.tidy.comp (hparam.prod .id')) have hf : ComputableTidilyInPolyTime f encBits encBits := (ComputableTidilyInPolyTime.of_eq (encIn := encPair encUnary encBits) (encMid := encBits) fun _ => rfl).comp (hparam.prod hpk) @@ -188,7 +188,7 @@ theorem SignatureScheme.OneTimeEUFCMA.exists_oneWay {S : SignatureScheme} (fun r : ((ℕ × List Bool) × ℕ) × List Bool => (r.1.1.1, r.2)) (encPair (encPair (encPair encUnary encBits) encUnary) encBits) (encPair encUnary encBits) := by polytime - exact (ComputableTidilyInPolyTime.snd encBits encBits).comp (heval.comp hprep) + exact (ComputableTidilyInPolyTime.snd encBits encBits).comp (heval.tidy.comp hprep) have hmsg : ComputableTidilyInPolyTime (fun r : ((ℕ × List Bool) × ℕ) × List Bool => List.replicate r.1.1.1 false) (encPair (encPair (encPair encUnary encBits) encUnary) encBits) encBits := by diff --git a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean index eb32ba7390..cbbe08c7c8 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean @@ -67,7 +67,7 @@ theorem eventually_prediction_entropy_le {f : List Bool → List Bool} (hf : One 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 (.of_tidy hefficient) c d 3) + (isPPT_wordInverter hf.polyTime hefficient c d 3) 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 diff --git a/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean index 800fffd0a8..db20865bf6 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/Seed.lean @@ -107,7 +107,7 @@ theorem exists_seedRealization (pair : SamplablePair) : Nonempty (SeedRealizatio refine ⟨{ length := fun n => c * (n + 1) ^ d length_isPolyTime := by polytime evaluate := evaluate - efficient := .of_tidy hefficient + efficient := hefficient distribution := ?_ }⟩ intro n rw [← pair.eval_sample] diff --git a/ComplexityTests/SeededEvaluator.lean b/ComplexityTests/SeededEvaluator.lean index aeb7b58ed3..73ccf72fc4 100644 --- a/ComplexityTests/SeededEvaluator.lean +++ b/ComplexityTests/SeededEvaluator.lean @@ -25,7 +25,7 @@ example : ∃ evaluate : ℕ → List Bool → List Bool, ∀ n coins, (evaluate n coins).length = n + 1 ∧ (evaluate n coins).headD false = true := by have hp : IsPPTOn encUnary encBits markedSample := by unfold markedSample; ppt obtain ⟨_, _, evaluate, hefficient, hsupported, _⟩ := hp.exists_total_seeded_evaluator - refine ⟨evaluate, .of_tidy hefficient, fun n coins => ?_⟩ + refine ⟨evaluate, hefficient, fun n coins => ?_⟩ have hs := hsupported n coins simp only [markedSample, ProbComp.eval_bind, BitString.eval_sampleList, ProbComp.eval_pure] at hs obtain ⟨word, hw, heq⟩ := (PMF.mem_support_map_iff _ _ _).mp hs @@ -47,7 +47,7 @@ example : ∃ (c d : ℕ) (evaluate : ℕ → List Bool → ℕ), return if bit then n else n + 1 have hp : IsPPTOn encUnary encUnary program := by dsimp only [program]; ppt obtain ⟨c, d, evaluate, hefficient, hsupported, hlaw⟩ := hp.exists_total_seeded_evaluator - refine ⟨c, d, evaluate, .of_tidy hefficient, ?_, ?_⟩ + refine ⟨c, d, evaluate, hefficient, ?_, ?_⟩ · intro n coins have hs := hsupported n coins simp only [program, ProbComp.eval_bind, ProbComp.eval_pure] at hs @@ -72,7 +72,7 @@ example : ∃ (c d : ℕ) (evaluate : List Bool → List Bool → List Bool), ProbComp.eval (ProbComp.uniform Bool) := by obtain ⟨c, d, evaluate, hefficient, hlaw⟩ := (isPPTOn_uniform_bool encBits).exists_padded_bool_coin_evaluator - exact ⟨c, d, evaluate, .of_tidy hefficient, fun a b length ha hb => + exact ⟨c, d, evaluate, hefficient, fun a b length ha hb => ⟨(hlaw a length ha).symm, (hlaw b length hb).symm⟩⟩ end ComplexityTests.SeededEvaluator diff --git a/abstracts/ComplexityAbstracts/CryptographyBridge.lean b/abstracts/ComplexityAbstracts/CryptographyBridge.lean index e4ca6136f9..feb4cee6a3 100644 --- a/abstracts/ComplexityAbstracts/CryptographyBridge.lean +++ b/abstracts/ComplexityAbstracts/CryptographyBridge.lean @@ -75,7 +75,7 @@ theorem strictPPT_iff {α β : Type} {a : α ↪ List Bool} {b : β ↪ List Boo using (hlaw x).symm · rintro ⟨program, hp, hlaw⟩ obtain ⟨c, d, evaluate, hevaluate, heq⟩ := hp.exists_seeded_evaluator - exact ⟨c, d, evaluate, polyTime_iff.mpr hevaluate, + exact ⟨c, d, evaluate, hevaluate, fun x => (hlaw x).symm.trans (heq x)⟩ theorem indistinguishable_iff {X Y : ℕ → PMF (List Bool)} : From be2a1d621936274ce6fa2a0c1426cbdb29db60b6 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 17:36:19 +0000 Subject: [PATCH 09/11] wip: relative pseudoentropy gap --- .../Computational/Pseudoentropy/Basic.lean | 38 ++++ .../Computational/Pseudoentropy/OneWay.lean | 178 +++++++++++++++--- .../Pseudoentropy/WordReduction.lean | 110 +++++++---- 3 files changed, 260 insertions(+), 66 deletions(-) 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 eb32ba7390..0795ea79b7 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean @@ -9,7 +9,7 @@ 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 @@ -18,21 +18,28 @@ import Complexity.Crypto.Negligible.Basic 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 +61,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 (.of_tidy 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 +139,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 +205,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) From a386eeca13a22c79689e7cd2d2e73719830cbfa0 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 17:39:26 +0000 Subject: [PATCH 10/11] chore(ci): lower the tidy-surface baseline for CoinTape --- scripts/tidy_surface_baseline.json | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/tidy_surface_baseline.json b/scripts/tidy_surface_baseline.json index a46905ca9d..924417edd8 100644 --- a/scripts/tidy_surface_baseline.json +++ b/scripts/tidy_surface_baseline.json @@ -47,7 +47,6 @@ "Complexity/Computability/Machines/Turing/MultiTape/Universal/PolyTime.lean": 4, "Complexity/Computability/Machines/Turing/MultiTape/Universal/SpaceBudget.lean": 2, "Complexity/Computability/Probabilistic/Adaptive.lean": 5, - "Complexity/Computability/Probabilistic/CoinTape.lean": 5, "Complexity/Computability/Probabilistic/Oracle.lean": 1, "Complexity/Computability/Probabilistic/Oracle/Composition.lean": 12, "Complexity/Computability/Probabilistic/Oracle/Iteration.lean": 3, From c3cd5cbe2619fe8b3ee4c6a86e590a88cc23eb51 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Mon, 2 Nov 2026 17:39:34 +0000 Subject: [PATCH 11/11] feat(Crypto): relativize the pseudoentropy gap to fixed advice --- .../Crypto/Computational/Pseudoentropy/OneWay.lean | 1 + ComplexityTests/Crypto/Nonuniform.lean | 9 +++++++++ 2 files changed, 10 insertions(+) diff --git a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean index 0795ea79b7..ca7eb41afd 100644 --- a/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean +++ b/Complexity/Crypto/Computational/Pseudoentropy/OneWay.lean @@ -12,6 +12,7 @@ import Complexity.Languages.Probabilistic.Notation 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 diff --git a/ComplexityTests/Crypto/Nonuniform.lean b/ComplexityTests/Crypto/Nonuniform.lean index f818b494b6..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 @@ -75,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