Reconstructions of the Nisan–Wigderson generator and list decoding

With its random choices fixed, the predictor that the Nisan–Wigderson reconstruction builds from a deterministic test needs the hard function f only through the earlier output bits, and by Cslib.Crypto.PRG.NisanWigderson.dependsOn_generator_extend each of them is a function of the at most a input bits that its block shares with the block of the predicted bit. A reconstruction stores these functions as tables, together with the position of the predicted bit, the candidate bit and the padding bits after that position; its guess is computed from this data and the test alone (Cslib.Crypto.PRG.NisanWigderson.Reconstruction.guess). Every trial gives a reconstruction with the same guess (Cslib.Crypto.PRG.NisanWigderson.Reconstruction.guess_ofTrial), and a reconstruction at position i consists of reconstructionBits D i ≤ m 2 ^ a bits (Cslib.Crypto.PRG.NisanWigderson.reconstructionBits_le).

If f is the codeword C.encode x of a message x in a list code C, a guess that agrees with f on a 1 / 2 + δ fraction of the inputs lists x among its candidates when C list decodes up to radius 1 / 2 - δ. With the sampling layer (Cslib.Crypto.PRG.NisanWigderson.div_two_mul_le_dens_goodTrials), a uniformly random trial lists x with probability at least ε / (2 m) (Cslib.Crypto.PRG.NisanWigderson.div_two_mul_le_dens_mem_candidates), and k independent trials give at most k L candidates (Cslib.Crypto.PRG.NisanWigderson.card_trialCandidates_le) that include x with probability at least 1 - (1 - ε / (2 m)) ^ k (Cslib.Crypto.PRG.NisanWigderson.one_sub_pow_le_dens_mem_trialCandidates): this is the randomized list-decoding reconstruction of [Hir18].

Main definitions

• Cslib.Crypto.PRG.NisanWigderson.Reconstruction: the data of a predictor, with the earlier output bits stored as tables.
• Cslib.Crypto.PRG.NisanWigderson.Reconstruction.guess: its guess.
• Cslib.Crypto.PRG.NisanWigderson.Reconstruction.ofTrial: the reconstruction of a trial.
• Cslib.Crypto.PRG.NisanWigderson.reconstructionBits: the number of bits of a reconstruction.
• Cslib.Crypto.PRG.NisanWigderson.trialCandidates: the candidates listed by several trials.

Main results

• Cslib.Crypto.PRG.NisanWigderson.Reconstruction.guess_ofTrial: a reconstruction guesses as its trial does.
• Cslib.Crypto.PRG.NisanWigderson.reconstructionBits_le: a reconstruction has at most m 2 ^ a bits.
• Cslib.Crypto.PRG.NisanWigderson.div_two_mul_le_dens_mem_candidates, Cslib.Crypto.PRG.NisanWigderson.one_sub_pow_le_dens_mem_trialCandidates: randomized list decoding.

References

• S. Hirahara, Non-black-box worst-case to average-case reductions within NP
• N. Nisan, A. Wigderson, Hardness vs randomness
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapters 19 and 20

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

A reconstruction for the design D: the data of the predictor that the reconstruction builds from a deterministic test, with its random choices fixed and the earlier output bits stored as tables.

• pos : Fin m

  The position of the predicted bit.

• table (j : Fin ↑self.pos) : (↥(D.overlap self.pos (Fin.castLE ⋯ j)) → Bool) → Bool

  For each earlier position j, output bit j as a function of the input bits in D.overlap pos j.

• bit : Bool

  The candidate value of the predicted bit.

• tail : { j : Fin m // self.pos < j } → Bool

  The padding bits after position pos.

def Cslib.Crypto.PRG.NisanWigderson.Reconstruction.pad {ℓ n a m : ℕ} {D : Design ℓ n a m} (R : Reconstruction D) (j : Fin m) : Bool

The padding of a reconstruction as a string of m bits, false up to position pos.

def Cslib.Crypto.PRG.NisanWigderson.Reconstruction.guess {ℓ n a m : ℕ} {D : Design ℓ n a m} (R : Reconstruction D) (test : (Fin m → Bool) → Bool) (x : Fin n → Bool) : Bool

The guess of a reconstruction at the input x: the test is run on the table values at x for the positions before pos, the candidate bit at pos, and the padding after pos; the guess is the candidate bit if the test accepts and its negation otherwise (nextBitGuess).

def Cslib.Crypto.PRG.NisanWigderson.Reconstruction.ofTrial {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (t : Trial ℓ m) : Reconstruction D

The reconstruction of the trial t for the hard function f: the table of output bit j is read off the generator on the seed that agrees with t.seed outside the t.pos-th block.

theorem Cslib.Crypto.PRG.NisanWigderson.Reconstruction.guess_ofTrial {ℓ n a m : ℕ} {D : Design ℓ n a m} (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (t : Trial ℓ m) : (ofTrial D f t).guess test = trialGuess D f test t

The reconstruction of a trial guesses as the trial does.

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

The number of bits of a reconstruction at position i: 2 ^ #(D.overlap i j) table entries for each earlier position j, then m - i - 1 padding bits and the candidate bit.

theorem Cslib.Crypto.PRG.NisanWigderson.reconstructionBits_le {ℓ n a m : ℕ} (D : Design ℓ n a m) (i : Fin m) : reconstructionBits D i ≤ m * 2 ^ a

A reconstruction has at most m 2 ^ a bits.

Randomized list decoding

def Cslib.Crypto.PRG.NisanWigderson.trialCandidates {ℓ n a m : ℕ} {α : Type u_1} {L : ℕ} [DecidableEq α] (C : ListCode α (Fin n → Bool) Bool L) (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) {k : ℕ} (ts : Fin k → Trial ℓ m) : Finset α

The candidates listed by the trials ts: the union of the candidates that the list code C decodes from their guesses.

theorem Cslib.Crypto.PRG.NisanWigderson.card_trialCandidates_le {ℓ n a m : ℕ} {α : Type u_1} {L : ℕ} [DecidableEq α] (C : ListCode α (Fin n → Bool) Bool L) (D : Design ℓ n a m) (test : (Fin m → Bool) → Bool) (f : (Fin n → Bool) → Bool) {k : ℕ} (ts : Fin k → Trial ℓ m) : (trialCandidates C D f test ts).card ≤ k * L

List size. k trials list at most k L candidates.

theorem Cslib.Crypto.PRG.NisanWigderson.div_two_mul_le_dens_mem_candidates {ℓ n a m : ℕ} {α : Type u_1} {L : ℕ} [DecidableEq α] (C : ListCode α (Fin n → Bool) Bool L) (D : Design ℓ n a m) (test : (Fin m → Bool) → Bool) (hm : 0 < m) {ε : ℝ} (hε₀ : 0 ≤ ε) (hC : C.ListDecodes (1 / 2 - ε / (2 * ↑m))) {x : α} (hε : ε ≤ (((generator D (C.encode x)).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) : ε / (2 * ↑m) ≤ ↑{t : Trial ℓ m | x ∈ C.candidates (trialGuess D (C.encode x) test t)}.dens

Sampling and list decoding [Hir18]. Let 0 < m, 0 ≤ ε, let the list code C list decode up to radius 1 / 2 - ε / (2 m), and let a deterministic test accept outputs of the generator built from the codeword of x with probability at least ε more than uniform strings. Then C lists x among the candidates for the guess of a uniformly random trial with probability at least ε / (2 m).

theorem Cslib.Crypto.PRG.NisanWigderson.one_sub_pow_le_dens_mem_trialCandidates {ℓ n a m : ℕ} {α : Type u_1} {L : ℕ} [DecidableEq α] (C : ListCode α (Fin n → Bool) Bool L) (D : Design ℓ n a m) (test : (Fin m → Bool) → Bool) (hm : 0 < m) {ε : ℝ} (hε₀ : 0 ≤ ε) (hC : C.ListDecodes (1 / 2 - ε / (2 * ↑m))) {x : α} (hε : ε ≤ (((generator D (C.encode x)).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) (k : ℕ) : 1 - (1 - ε / (2 * ↑m)) ^ k ≤ ↑{ts : Fin k → Trial ℓ m | x ∈ trialCandidates C D (C.encode x) test ts}.dens

Repeated sampling and list decoding [Hir18]. Under the hypotheses of div_two_mul_le_dens_mem_candidates, the at most k L candidates listed by k independent uniformly random trials include x with probability at least 1 - (1 - ε / (2 m)) ^ k.