The Nisan–Wigderson generator for derandomization

Derandomizing a polynomial-time algorithm with the Nisan–Wigderson generator [NW94] needs two ingredients beyond the reconstruction of Cslib.Crypto.PRG.NisanWigderson.toReal_realExperiment_sub_toReal_idealExperiment_lt.

Designs with seeds of linear length. The algorithm runs over all 2 ^ ℓ seeds, so the seed length ℓ must be logarithmic in the running time, hence linear in the input length n of the hard function. The polynomial designs of Cslib.Crypto.PRG.NisanWigderson.Design.polynomial have ℓ = n ^ 2. Here designs are built greedily Arora and Barak, Chapter 20, as masks: lists of ℓ bits, the block of a mask being the set of positions where it is true. greedyMasks ℓ n a runs through all masks of length ℓ in the order of Cslib.BitString.enumList and keeps a mask when it has n ones and shares at most a of them with every mask kept before. The result is maximal: every mask with n ones shares more than a of them with some kept mask. Counting the n-sets that share a + 1 elements with a given block shows that the greedy design has at least C(ℓ, a + 1) / C(n, a + 1) ^ 2 blocks (choose_le_length_greedyMasks_mul), so with ℓ = (b + 1) t and a + 1 = t it has at least b ^ t / 4 ^ n blocks (le_length_greedyMasks). The construction is a simple loop over lists, whose running time is polynomial in 2 ^ ℓ, and so is the generator on lists listGenerator, which reads the bits of the seed at the ones of each mask (restrictMask) and applies the hard function; its polynomial-time certificates are in Complexity/Computability/Complexity/Classes/BPP/Derandomization/Generator.lean.

Fooling in counting form. For an average-case hard function f (Cslib.Circuits.Boolean.IsAverageCaseHard), the fraction of seeds on which a small test accepts the output of the generator is within ε of the fraction of all strings it accepts (abs_card_div_sub_card_div_lt). The hardness hypothesis is non-strict, as produced by Yao's XOR lemma, and the strict bound needed by the reconstruction comes from the slack m < ε s between the number m of output bits and the hardness s.

Main definitions

• Cslib.Crypto.PRG.NisanWigderson.overlapCount, Cslib.Crypto.PRG.NisanWigderson.maskBlock, Cslib.Crypto.PRG.NisanWigderson.restrictMask: the common ones of two masks, the block of a mask, and the bits of a string at the ones of a mask.
• Cslib.Crypto.PRG.NisanWigderson.Design.ofMasks: the design whose blocks are given by masks.
• Cslib.Crypto.PRG.NisanWigderson.greedyMasks: the greedy design, as a list of masks.
• Cslib.Crypto.PRG.NisanWigderson.Design.greedy: its first m blocks, as a design.
• Cslib.Crypto.PRG.NisanWigderson.listGenerator: the generator on lists, for a function on words and a list of masks.

Main results

• Cslib.Crypto.PRG.NisanWigderson.ofFn_restrict_ofMasks: reading a block of a design given by masks is restrictMask.
• Cslib.Crypto.PRG.NisanWigderson.exists_mem_greedyMasks_lt_overlapCount: the greedy design is maximal.
• Cslib.Crypto.PRG.NisanWigderson.choose_le_length_greedyMasks_mul, Cslib.Crypto.PRG.NisanWigderson.le_length_greedyMasks: the greedy design is large.
• Cslib.Crypto.PRG.NisanWigderson.listGenerator_take_greedyMasks: with the greedy masks, the generator on lists is the Nisan–Wigderson generator of Design.greedy.
• Cslib.Crypto.PRG.NisanWigderson.abs_card_div_sub_card_div_lt: for an average-case hard function, the generator fools small circuits, as a statement about counts.

References

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

Masks

def Cslib.Crypto.PRG.NisanWigderson.overlapCount (v w : List Bool) : ℕ

The number of positions where both v and w are true.

def Cslib.Crypto.PRG.NisanWigderson.maskBlock (ℓ : ℕ) (w : List Bool) : Finset (Fin ℓ)

The block of positions in Fin ℓ where the mask w is true.

def Cslib.Crypto.PRG.NisanWigderson.restrictMask (w z : List Bool) : List Bool

The bits of z at the positions where the mask w is true, in increasing order of position.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.mem_maskBlock {ℓ : ℕ} {w : List Bool} {k : Fin ℓ} : k ∈ maskBlock ℓ w ↔ w.getD (↑k) false = true

theorem Cslib.Crypto.PRG.NisanWigderson.count_true_eq_card_maskBlock (w : List Bool) : List.count true w = (maskBlock w.length w).card

The ones of a mask are the elements of its block.

theorem Cslib.Crypto.PRG.NisanWigderson.count_true_eq_card_maskBlock_of_length {ℓ : ℕ} {w : List Bool} (h : w.length = ℓ) : List.count true w = (maskBlock ℓ w).card

The ones of a mask of length ℓ are the elements of its block in Fin ℓ.

theorem Cslib.Crypto.PRG.NisanWigderson.overlapCount_eq_card_inter {ℓ : ℕ} {v w : List Bool} (hv : v.length = ℓ) (hw : w.length = ℓ) : overlapCount v w = (maskBlock ℓ v ∩ maskBlock ℓ w).card

Two masks of length ℓ have as many common ones as their blocks have common elements.

theorem Cslib.Crypto.PRG.NisanWigderson.overlapCount_self (w : List Bool) : overlapCount w w = List.count true w

A mask shares all its ones with itself.

theorem Cslib.Crypto.PRG.NisanWigderson.overlapCount_comm (v w : List Bool) : overlapCount v w = overlapCount w v

Sharing ones is symmetric.

Designs given by masks

def Cslib.Crypto.PRG.NisanWigderson.Design.ofMasks {ℓ n a m : ℕ} (masks : Fin m → List Bool) (length_masks : ∀ (i : Fin m), (masks i).length = ℓ) (count_masks : ∀ (i : Fin m), List.count true (masks i) = n) (overlapCount_masks : ∀ (i j : Fin m), i ≠ j → overlapCount (masks i) (masks j) ≤ a) : Design ℓ n a m

The design whose i-th block is the block of the mask masks i, for masks of length ℓ with n ones each, any two of which share at most a ones.

theorem Cslib.Crypto.PRG.NisanWigderson.ofFn_restrict_ofMasks {ℓ n a m : ℕ} (masks : Fin m → List Bool) (length_masks : ∀ (i : Fin m), (masks i).length = ℓ) (count_masks : ∀ (i : Fin m), List.count true (masks i) = n) (overlapCount_masks : ∀ (i j : Fin m), i ≠ j → overlapCount (masks i) (masks j) ≤ a) (i : Fin m) (z : Fin ℓ → Bool) : List.ofFn ((Design.ofMasks masks length_masks count_masks overlapCount_masks).restrict i z) = restrictMask (masks i) (List.ofFn z)

Reading a block given by a mask. The bits of a seed z in the block of a design given by masks are the bits of z at the ones of the mask, in increasing order of position.

The greedy design

def Cslib.Crypto.PRG.NisanWigderson.greedyStep (n a : ℕ) (kept : List (List Bool)) (w : List Bool) : List (List Bool)

One step of the greedy construction of a design: keep the candidate mask w when it has n ones and shares at most a of them with every mask kept so far.

def Cslib.Crypto.PRG.NisanWigderson.greedyMasks (ℓ n a : ℕ) : List (List Bool)

The greedy design Arora and Barak, Chapter 20, as masks: the masks of length ℓ, in the order of Cslib.BitString.enumList, each kept when it has n ones and shares at most a of them with every mask kept before it.

theorem Cslib.Crypto.PRG.NisanWigderson.length_of_mem_greedyMasks {ℓ n a : ℕ} {w : List Bool} (hw : w ∈ greedyMasks ℓ n a) : w.length = ℓ

Every mask of the greedy design has length ℓ.

theorem Cslib.Crypto.PRG.NisanWigderson.count_of_mem_greedyMasks {ℓ n a : ℕ} {w : List Bool} (hw : w ∈ greedyMasks ℓ n a) : List.count true w = n

Every mask of the greedy design has n ones.

theorem Cslib.Crypto.PRG.NisanWigderson.pairwise_greedyMasks {ℓ n a : ℕ} : List.Pairwise (fun (u v : List Bool) => overlapCount v u ≤ a) (greedyMasks ℓ n a)

Each mask of the greedy design shares at most a ones with every earlier one.

theorem Cslib.Crypto.PRG.NisanWigderson.exists_mem_greedyMasks_lt_overlapCount {ℓ n a : ℕ} {w : List Bool} (han : a < n) (hw : w.length = ℓ) (hn : List.count true w = n) : ∃ v ∈ greedyMasks ℓ n a, a < overlapCount w v

The greedy design is maximal. If a < n, every mask of length ℓ with n ones shares more than a ones with some mask of the greedy design.

theorem Cslib.Crypto.PRG.NisanWigderson.choose_le_length_greedyMasks_mul {ℓ n a : ℕ} (han : a < n) (hnℓ : n ≤ ℓ) : ℓ.choose (a + 1) ≤ (greedyMasks ℓ n a).length * n.choose (a + 1) ^ 2

The greedy design is large. If a < n ≤ ℓ, the greedy design has at least C(ℓ, a + 1) / C(n, a + 1) ^ 2 masks: by maximality every set of n elements of Fin ℓ shares a + 1 elements with some block, and a block shares a + 1 elements with at most C(n, a + 1) C(ℓ - a - 1, n - a - 1) of them.

theorem Cslib.Crypto.PRG.NisanWigderson.le_length_greedyMasks {n m b t : ℕ} (ht : 0 < t) (htn : t ≤ n) (hn : n ≤ (b + 1) * t) (hm : 4 ^ n * m ≤ b ^ t) : m ≤ (greedyMasks ((b + 1) * t) n (t - 1)).length

The greedy design with seeds of linear length. If 0 < t ≤ n ≤ (b + 1) t and 4 ^ n m ≤ b ^ t, the greedy design on seeds of (b + 1) t bits, with blocks of n positions sharing at most t - 1 of them, has at least m blocks.

def Cslib.Crypto.PRG.NisanWigderson.Design.greedy (ℓ n a m : ℕ) (h : m ≤ (greedyMasks ℓ n a).length) : Design ℓ n a m

The first m masks of the greedy design, as a design, when there are at least m.

theorem Cslib.Crypto.PRG.NisanWigderson.ofFn_restrict_greedy {ℓ n a m : ℕ} (h : m ≤ (greedyMasks ℓ n a).length) (i : Fin m) (z : Fin ℓ → Bool) : List.ofFn ((Design.greedy ℓ n a m h).restrict i z) = restrictMask (greedyMasks ℓ n a)[i] (List.ofFn z)

Reading block i of the greedy design is restrictMask with the i-th greedy mask.

def Cslib.Crypto.PRG.NisanWigderson.listGenerator (g : List Bool → Bool) (n : ℕ) (masks : List (List Bool)) (z : List Bool) : List Bool

The Nisan–Wigderson generator on lists: for each mask w of masks, the value of g on the first n bits of the seed z at the ones of w.

theorem Cslib.Crypto.PRG.NisanWigderson.listGenerator_take_greedyMasks {ℓ n a m : ℕ} (h : m ≤ (greedyMasks ℓ n a).length) (g : List Bool → Bool) (z : Fin ℓ → Bool) : listGenerator g n (List.take m (greedyMasks ℓ n a)) (List.ofFn z) = List.ofFn ((generator (Design.greedy ℓ n a m h) fun (x : Fin n → Bool) => g (List.ofFn x)) z)

With the first m masks of the greedy design, the generator on lists is the Nisan–Wigderson generator of Design.greedy and of the function g on words of n bits.

Fooling small circuits, in counting form

theorem Cslib.Crypto.PRG.NisanWigderson.abs_card_div_sub_card_div_lt {ℓ n a m : ℕ} (D : Design ℓ n a m) {f : BooleanFunction n} {s S : ℕ} {ε : ℝ} (hf : Circuits.Boolean.IsAverageCaseHard f s) (hs : S + 1 + m * (2 ^ a * (2 * a + 3) + 1) + 1 ≤ s) (hm : ↑m < ε * ↑s) (test : BooleanFunction m) (htest : Circuits.complexity Circuits.Boolean.interpretation (Circuits.single test) ≤ S) : |↑{z : Fin ℓ → Bool | test ((generator D f) z) = true}.card / 2 ^ ℓ - ↑{r : BitString m | test r = true}.card / 2 ^ m| < ε

The Nisan–Wigderson generator fools small circuits, in counting form [NW94]. Let f be average-case hard for size s (with the non-strict bound of Cslib.Circuits.Boolean.IsAverageCaseHard), let S + 1 + m (2 ^ a (2 a + 3) + 1) + 1 ≤ s, and let m < ε s. Then for every test of De Morgan circuit complexity at most S, the fraction of the 2 ^ ℓ seeds on which the test accepts the output of the generator differs from the fraction of the 2 ^ m strings it accepts by less than ε. The slack m < ε s makes the agreement bound 1 / 2 + 1 / s strictly smaller than the 1 / 2 + ε / m of the reconstruction.