The Nisan–Wigderson generator and its reconstruction

An (ℓ, n, a)-design with m blocks is a family of m subsets of Fin ℓ, each with n elements, any two of which share at most a elements. Given such a design and a Boolean function f on n bits, the Nisan–Wigderson generator stretches a seed z of ℓ bits to the m bits f (z|S₀) … f (z|Sₘ₋₁), where z|S lists the bits of z in S in increasing order of position [NW94], Arora and Barak, Chapter 20.

Its analysis is a reconstruction. Suppose that a test accepts generated outputs with probability at least ε more than uniform ones. By the next-bit theorem (Cslib.Crypto.PRG.Generator.exists_half_add_div_le_predictionExperiment), the predictor built from the test guesses some bit i from the bits before it with probability at least 1 / 2 + ε / m. This probability is an average over seeds, and a seed consists of the input x = z|Sᵢ of bit i together with the bits outside Sᵢ, so for some choice of the bits outside Sᵢ the predictor still guesses f x from the earlier bits with probability at least 1 / 2 + ε / m. Once the bits outside Sᵢ are fixed, each earlier bit j < i depends on x only through the at most a positions of Sᵢ ∩ Sⱼ, so as a function of x it is given by a table of at most 2 ^ a values of f. For a deterministic test, fixing the random choices of the predictor as well yields a function that agrees with f on at least a 1 / 2 + ε / m fraction of the inputs and is computed by the test from i functions of at most a input bits each. A lower bound on the size of circuits approximating f thus becomes a lower bound on the size of circuits distinguishing the generator; this file is the finite core of that argument, without a model of computation.

Designs with good parameters exist (Cslib.Crypto.PRG.NisanWigderson.Design.nonempty_four_mul_sq).

Main definitions

• Cslib.Crypto.PRG.NisanWigderson.Design: an (ℓ, n, a)-design with m blocks.
• Cslib.Crypto.PRG.NisanWigderson.Design.restrict, Cslib.Crypto.PRG.NisanWigderson.Design.extend: reading a block of a string, and overwriting it.
• Cslib.Crypto.PRG.NisanWigderson.Design.overlap: the positions of one block lying in another.
• Cslib.Crypto.PRG.NisanWigderson.generator: the Nisan–Wigderson generator.
• Cslib.Crypto.PRG.NisanWigderson.hardwiredExperiment: the prediction experiment for bit i with the seed bits outside the i-th block fixed.

Main results

• Cslib.Crypto.PRG.NisanWigderson.predictionExperiment_generator: the prediction experiment is the average of the hardwired experiments, so Cslib.Crypto.PRG.NisanWigderson.exists_predictionExperiment_le_hardwiredExperiment some hardwiring does at least as well.
• Cslib.Crypto.PRG.NisanWigderson.dependsOn_generator_extend, Cslib.Crypto.PRG.NisanWigderson.Design.card_overlap_le: with the bits outside block i fixed, output bit j ≠ i depends on at most a bits of the input of bit i.
• Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_hardwiredExperiment: the reconstruction for randomized tests, in the language of the next-bit test.
• Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_card_nextBitGuess_eq, Cslib.Crypto.PRG.NisanWigderson.exists_dependsOn_half_add_div_le_card_nextBitGuess_eq: the reconstruction for deterministic tests, as a statement about functions: f agrees on a 1 / 2 + ε / m fraction of inputs with a function computed by the test from i functions of at most a input bits each.

References

• N. Nisan, A. Wigderson, Hardness vs randomness
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 20

structure Cslib.Crypto.PRG.NisanWigderson.Design (ℓ n a m : ℕ) : Type

An (ℓ, n, a)-design with m blocks Arora and Barak, Chapter 20: m subsets of Fin ℓ, each with n elements, any two distinct ones sharing at most a elements.

• block : Fin m → Finset (Fin ℓ)

  The i-th block of the design.

• card_block (i : Fin m) : (self.block i).card = n

  Every block has n elements.

• card_inter_le {i j : Fin m} : i ≠ j → (self.block i ∩ self.block j).card ≤ a

  Two distinct blocks share at most a elements.

def Cslib.Crypto.PRG.NisanWigderson.Design.restrict {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (z : Fin ℓ → α) : Fin n → α

The bits of z in the i-th block of D, in increasing order of position.

def Cslib.Crypto.PRG.NisanWigderson.Design.extend {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (x : Fin n → α) (w : Fin ℓ → α) : Fin ℓ → α

The string that agrees with w outside the i-th block of D and carries the bits of x on it, in increasing order of position.

def Cslib.Crypto.PRG.NisanWigderson.Design.overlap {ℓ n a m : ℕ} (D : Design ℓ n a m) (i j : Fin m) : Finset (Fin n)

The positions in the i-th block of D, counted in increasing order, of the elements that also lie in the j-th block.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.restrict_apply {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (z : Fin ℓ → α) (k : Fin n) : D.restrict i z k = z (((D.block i).orderEmbOfFin ⋯) k)

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.extend_apply_orderEmbOfFin {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (x : Fin n → α) (w : Fin ℓ → α) (k : Fin n) : D.extend i x w (((D.block i).orderEmbOfFin ⋯) k) = x k

theorem Cslib.Crypto.PRG.NisanWigderson.Design.extend_apply_of_notMem {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (x : Fin n → α) (w : Fin ℓ → α) {k : Fin ℓ} (hk : k ∉ D.block i) : D.extend i x w k = w k

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.restrict_extend {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (x : Fin n → α) (w : Fin ℓ → α) : D.restrict i (D.extend i x w) = x

Reading the i-th block of a string whose i-th block was overwritten by x gives x.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.extend_restrict {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (z : Fin ℓ → α) : D.extend i (D.restrict i z) z = z

Overwriting the i-th block of z by its own bits gives z.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.Design.extend_extend {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i : Fin m) (x y : Fin n → α) (w : Fin ℓ → α) : D.extend i y (D.extend i x w) = D.extend i y w

Overwriting the i-th block twice keeps only the second overwrite.

theorem Cslib.Crypto.PRG.NisanWigderson.Design.card_overlap {ℓ n a m : ℕ} (D : Design ℓ n a m) (i j : Fin m) : (D.overlap i j).card = (D.block i ∩ D.block j).card

The positions of the i-th block lying in the j-th block are as many as the elements the two blocks share.

theorem Cslib.Crypto.PRG.NisanWigderson.Design.card_overlap_le {ℓ n a m : ℕ} (D : Design ℓ n a m) {i j : Fin m} (hij : i ≠ j) : (D.overlap i j).card ≤ a

For distinct blocks, at most a positions of the i-th block lie in the j-th block.

theorem Cslib.Crypto.PRG.NisanWigderson.Design.dependsOn_restrict_extend {ℓ n a m : ℕ} {α : Type u_1} (D : Design ℓ n a m) (i j : Fin m) (w : Fin ℓ → α) : DependsOn (fun (x : Fin n → α) => D.restrict j (D.extend i x w)) ↑(D.overlap i j)

With the bits outside the i-th block fixed to those of w, the bits in the j-th block depend on the bits x in the i-th block only through the positions in D.overlap i j.

def Cslib.Crypto.PRG.NisanWigderson.generator {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) : Generator (Fin ℓ → Bool) (Fin m → Bool)

The Nisan–Wigderson generator of a design D and a function f on n bits Arora and Barak, Chapter 20: bit i of the output on a seed z is f applied to the bits of z in the i-th block.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.generator_apply {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (z : Fin ℓ → Bool) (i : Fin m) : (generator D f) z i = f (D.restrict i z)

theorem Cslib.Crypto.PRG.NisanWigderson.dependsOn_generator_extend {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (i j : Fin m) (w : Fin ℓ → Bool) : DependsOn (fun (x : Fin n → Bool) => (generator D f) (D.extend i x w) j) ↑(D.overlap i j)

With the bits outside the i-th block fixed to those of w, output bit j of the generator depends on the bits x in the i-th block only through the positions in D.overlap i j. For j ≠ i there are at most a of them (Design.card_overlap_le).

noncomputable def Cslib.Crypto.PRG.NisanWigderson.hardwiredExperiment {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (i : Fin m) (w : Fin ℓ → Bool) (predictor : Adversary (Fin ↑i → Bool)) : PMF Bool

The prediction experiment for bit i of the generator with the seed bits outside the i-th block fixed to those of w: the input x of bit i is uniform, the predictor receives the first i bits of the output on the seed D.extend i x w, and the experiment outputs true exactly when the predictor's guess is f x.

theorem Cslib.Crypto.PRG.NisanWigderson.predictionExperiment_generator {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : (generator D f).predictionExperiment i predictor = do let w ← Probability.PMF.uniformOfFintype (Fin ℓ → Bool) hardwiredExperiment D f i w predictor

The prediction experiment for bit i of the generator is the average, over a uniform w, of the experiments with the seed bits outside the i-th block fixed to those of w.

theorem Cslib.Crypto.PRG.NisanWigderson.exists_predictionExperiment_le_hardwiredExperiment {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (i : Fin m) (predictor : Adversary (Fin ↑i → Bool)) : ∃ (w : Fin ℓ → Bool), ((generator D f).predictionExperiment i predictor) true ≤ (hardwiredExperiment D f i w predictor) true

Hardwiring. Some choice of the seed bits outside the i-th block keeps the probability that a predictor guesses bit i of the generator correctly.

theorem Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_hardwiredExperiment {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (adversary : Adversary (Fin m → Bool)) (hm : 0 < m) {ε : ℝ} (hε : ε ≤ (((generator D f).realExperiment adversary) true).toReal - ((Generator.idealExperiment adversary) true).toReal) : ∃ (i : Fin m) (w : Fin ℓ → Bool), 1 / 2 + ε / ↑m ≤ ((hardwiredExperiment D f i w (nextBitPredictor adversary i)) true).toReal

The Nisan–Wigderson reconstruction Arora and Barak, Chapter 20. If 0 < m and a test accepts outputs of the generator with probability at least ε more than uniform strings, then for some position i and some choice w of the seed bits outside the i-th block, the predictor built from the test guesses f x from the first i bits of the output on D.extend i x w with probability at least 1 / 2 + ε / m, for a uniform x. By dependsOn_generator_extend and Design.card_overlap_le, each of these i bits depends on at most a bits of x.

theorem Cslib.Crypto.PRG.NisanWigderson.hardwiredExperiment_nextBitPredictor_pure {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (i : Fin m) (w : Fin ℓ → Bool) : hardwiredExperiment D f i w (nextBitPredictor (fun (y : Fin m → Bool) => PMF.pure (test y)) i) = do let r ← Probability.PMF.uniformOfFintype Bool let u ← Probability.PMF.uniformOfFintype (Fin m → Bool) PMF.map (fun (x : Fin n → Bool) => decide (nextBitGuess test i r u (Fin.take ↑i ⋯ ((generator D f) (D.extend i x w))) = f x)) (Probability.PMF.uniformOfFintype (Fin n → Bool))

The hardwired experiment against the predictor built from a deterministic test, with the random choices of the predictor drawn first.

theorem Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_card_nextBitGuess_eq {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (hm : 0 < m) {ε : ℝ} (hε : ε ≤ (((generator D f).realExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal - ((Generator.idealExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal) : ∃ (i : Fin m) (w : Fin ℓ → Bool) (r : Bool) (u : Fin m → Bool), 1 / 2 + ε / ↑m ≤ ↑{x : Fin n → Bool | nextBitGuess test i r u (Fin.take ↑i ⋯ ((generator D f) (D.extend i x w))) = f x}.card / 2 ^ n

The Nisan–Wigderson reconstruction for deterministic tests, with explicit hardwiring. If 0 < m and a deterministic test accepts outputs of the generator with probability at least ε more than uniform strings, then for some position i, seed w, bit r and string u, the guess nextBitGuess test i r u on the first i bits of the output on D.extend i x w equals f x for at least a 1 / 2 + ε / m fraction of the inputs x.

theorem Cslib.Crypto.PRG.NisanWigderson.exists_dependsOn_half_add_div_le_card_nextBitGuess_eq {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (hm : 0 < m) {ε : ℝ} (hε : ε ≤ (((generator D f).realExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal - ((Generator.idealExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal) : ∃ (i : Fin m) (s : Fin ↑i → Finset (Fin n)) (bit : Fin ↑i → (Fin n → Bool) → Bool) (r : Bool) (u : Fin m → Bool), (∀ (j : Fin ↑i), (s j).card ≤ a) ∧ (∀ (j : Fin ↑i), DependsOn (bit j) ↑(s j)) ∧ 1 / 2 + ε / ↑m ≤ ↑{x : Fin n → Bool | (nextBitGuess test i r u fun (j : Fin ↑i) => bit j x) = f x}.card / 2 ^ n

The Nisan–Wigderson reconstruction for deterministic tests, as a statement about functions. If 0 < m and a deterministic test accepts outputs of the generator with probability at least ε more than uniform strings, then for some position i there are a bit r, a string u, and i functions bit j on n bits, each depending only on a set s j of at most a positions, such that nextBitGuess test i r u (fun j => bit j x) = f x for at least a 1 / 2 + ε / m fraction of the inputs x.