Pseudorandomness and one-way functions
Complexity-theoretic foundations of cryptography and derandomization: one-way functions, hardcore predicates (Goldreich–Levin), hardness amplification (Yao's XOR lemma), hardness-versus-randomness generators (Nisan–Wigderson), and Impagliazzo's five worlds.
TheoremNisan-Wigderson: exponential hardness in E derandomizes BPP#●ready to prove
Suppose there are a decision problem \(f\) in E and a natural number \(c > 0\) such that, for every \(n\), every well-formed flat Boolean circuit \(C\) on \(n\) inputs without mod gates that computes \(f\) on all bitstrings of length \(n\) (for every bitstring \(x\) of length \(n\), the value of its last gate on input \(x\) is \(f(x)\)) satisfies \(|C|^c \ge 2^n\), where \(|C|\) is its number of gates; that is, \(C\) has at least \(2^{n/c}\) gates. Then BPP equals P.
public theorem_wanted nisan_wigderson :
(∃ f : List Bool → Bool, f ∈ E ∧ ∃ c : ℕ, 0 < c ∧
∀ n : ℕ, ∀ C : List (ACGate n), WellFormedCircuit C → IsModFree C →
(∀ x : List Bool, x.length = n →
(circuitEval C (fun i => x.getD (i : ℕ) false)).getLast? = some (f x)) →
C.length ^ c ≥ 2 ^ n) →
BPP = MetaMathlibExt.ComplexityTheory.Pdef E : DecisionComplexityClass :=
{L | ∃ c, langOf L ∈ Cslib.Turing.MultiTapeTM.DTIME (fun n => 2 ^ (c * n))}CSLibExt/Computability/Complexity/Classes.lean:129
inductive ACGate (n : ℕ) where
| var : Fin n → ACGate n
| const : Bool → ACGate n
| notGate : ℕ → ACGate n
| andGate : List ℕ → ACGate n
| orGate : List ℕ → ACGate n
| modGate : ℕ → List ℕ → ACGate nCSLibExt/Computability/Complexity/Classes.lean:414
def WellFormedCircuit {n : ℕ} (C : List (ACGate n)) : Prop :=
∀ j (h : j < C.length), ∀ a ∈ gateInputs (C[j]'h), a < jCSLibExt/Computability/Complexity/Classes.lean:432
def IsModFree {n : ℕ} (C : List (ACGate n)) : Prop :=
∀ g ∈ C, match g with
| .modGate _ _ => False
| _ => TrueCSLibExt/Computability/Complexity/Classes.lean:538
def circuitEval {n : ℕ} (C : List (ACGate n)) (assign : Fin n → Bool) : List Bool :=
C.foldl (fun vs g => vs ++ [gateValue vs assign g]) []CSLibExt/Computability/Complexity/Classes.lean:447
def BPP : DecisionComplexityClass :=
{L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
∀ x,
(L x = true →
3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
2 * 2 ^ (p.eval x.length)) ∧
(L x = false →
3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≤
2 ^ (p.eval x.length))}CSLibExt/Computability/Complexity/Classes.lean:199
def P : DecisionComplexityClass :=
{ L | IsPolyTime L }MathlibExt/Computability/Complexity.lean:194
Sources
- N. Nisan and A. Wigderson, "Hardness vs randomness", Journal of Computer and System Sciences 49 (1994), 149-167 (FOCS 1988).
TheoremOne-way functions imply P ≠ NP#●ready to prove
If some family \(f\), assigning to each natural number \(n\) and each \(n\)-bit string \(x\) a bitstring \(f_n(x)\), is a one-way function family, then \(\mathrm{P} \neq \mathrm{NP}\).
public theorem_wanted owf_implies_p_ne_np :
∀ f : (n : ℕ) → (Fin n → Bool) → List Bool, IsOneWayFunction f → P ≠ NPdef IsOneWayFunction (f : (n : ℕ) → (Fin n → Bool) → List Bool) : Prop :=
(∃ pOut : Polynomial ℕ, ∀ n, ∀ x : Fin n → Bool, (f n x).length ≤ pOut.eval n) ∧
(∃ evalf : List Bool → List Bool, IsPolyTime evalf ∧
∀ n, ∀ x : Fin n → Bool,
evalf (MetaMathlibExt.BitstringEncoding.bitEncode (n, List.ofFn x)) = f n x) ∧
∀ (q : Polynomial ℕ) (inv : ℕ × List Bool × List Bool → List Bool),
IsPolyTime inv → Negligible (fun n => invertSucc f inv n (q.eval n))CSLibExt/Computability/Complexity/Classes.lean:1090
def P : DecisionComplexityClass :=
{ L | IsPolyTime L }MathlibExt/Computability/Complexity.lean:194
def NP : DecisionComplexityClass :=
{ L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
IsPolyTime R ∧
∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }MathlibExt/Computability/Complexity.lean:200
Sources
- O. Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001, Section 2.2 (one-way functions imply P ≠ NP); R. Impagliazzo, "A personal view of average-case complexity", Proceedings of the Tenth Annual Structure in Complexities Theory Conference (1995), 134-147 (five worlds).
Uses 4
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.