The Nisan–Wigderson generator fools small circuits

This file adds circuit sizes to the reconstruction of Cslib.Crypto.PRG.NisanWigderson.exists_dependsOn_half_add_div_le_card_nextBitGuess_eq. The function reconstructed from a deterministic test runs the test on i functions of at most a input bits each, on constants, and possibly negates the result. A function of at most a input bits costs at most 2 ^ a (2 a + 3) + 1 De Morgan gates (Cslib.Circuits.Boolean.complexity_le_of_dependsOn), so if the test is computed with S gates, the reconstructed function is computed with at most S + m (2 ^ a (2 a + 3) + 1) + 1 gates (exists_complexity_le_half_add_div_le_card_eq). Contrapositively, if no circuit of that size agrees with f on a 1 / 2 + ε / m fraction of the inputs, then no test computed with S gates accepts outputs of the generator with probability ε more than uniform strings (toReal_realExperiment_sub_toReal_idealExperiment_lt). Gates are counted as in Cslib.Circuits.complexity over the De Morgan basis, constants and negations included.

Main results

• Cslib.Crypto.PRG.NisanWigderson.exists_complexity_le_half_add_div_le_card_eq: a test of circuit complexity S distinguishing the generator with advantage ε yields a circuit of complexity at most S + m (2 ^ a (2 a + 3) + 1) + 1 agreeing with f on a 1 / 2 + ε / m fraction of the inputs.
• Cslib.Crypto.PRG.NisanWigderson.toReal_realExperiment_sub_toReal_idealExperiment_lt: the generator fools circuits with S gates if f is hard to approximate with S + m (2 ^ a (2 a + 3) + 1) + 1 gates.

References

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

theorem Cslib.Crypto.PRG.NisanWigderson.exists_complexity_le_half_add_div_le_card_eq {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : BooleanFunction n) (test : BooleanFunction m) (hm : 0 < m) {ε : ℝ} (hε : ε ≤ (((generator D f).realExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal - ((Generator.idealExperiment fun (y : BitString m) => PMF.pure (test y)) true).toReal) : ∃ (g : BooleanFunction n), Circuits.complexity Circuits.Boolean.interpretation (Circuits.single g) ≤ Circuits.complexity Circuits.Boolean.interpretation (Circuits.single test) + m * (2 ^ a * (2 * a + 3) + 1) + 1 ∧ 1 / 2 + ε / ↑m ≤ ↑{x : BitString n | g x = f x}.card / 2 ^ n

The Nisan–Wigderson reconstruction with circuits Arora and Barak, Chapter 20. If 0 < m and a deterministic test accepts outputs of the generator with probability at least ε more than uniform strings, then some function g on n bits agrees with f on at least a 1 / 2 + ε / m fraction of the inputs and has De Morgan circuit complexity at most that of the test plus m * (2 ^ a * (2 * a + 3) + 1) + 1.

theorem Cslib.Crypto.PRG.NisanWigderson.toReal_realExperiment_sub_toReal_idealExperiment_lt {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : BooleanFunction n) (hm : 0 < m) {ε : ℝ} {S : ℕ} (hf : ∀ (g : BooleanFunction n), Circuits.complexity Circuits.Boolean.interpretation (Circuits.single g) ≤ S + m * (2 ^ a * (2 * a + 3) + 1) + 1 → ↑{x : BitString n | g x = f x}.card / 2 ^ n < 1 / 2 + ε / ↑m) (test : BooleanFunction m) (htest : Circuits.complexity Circuits.Boolean.interpretation (Circuits.single test) ≤ S) : (((generator D f).realExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal - ((Generator.idealExperiment fun (y : BitString m) => PMF.pure (test y)) true).toReal < ε

The Nisan–Wigderson generator fools small circuits Arora and Barak, Chapter 20. Let 0 < m. If every function on n bits of complexity at most S + m * (2 ^ a * (2 * a + 3) + 1) + 1 agrees with f on less than a 1 / 2 + ε / m fraction of the inputs, then every test of complexity at most S accepts outputs of the generator with probability less than ε more than uniform strings.