Sampling the advice of the Nisan–Wigderson reconstruction

The reconstruction Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_card_nextBitGuess_eq shows that, for a deterministic test with advantage ε against the Nisan–Wigderson generator, some choice of a position i, of the seed bits outside the i-th block, of a candidate bit for bit i and of padding bits after position i gives a guess that agrees with the hard function f on a 1 / 2 + ε / m fraction of the inputs. Here these choices are sampled instead, as in the randomized reconstruction of [Hir18]: a trial t collects them, and its agreement trialAgreement D f test t is the fraction of the inputs on which its guess is correct. Probabilities are densities (Finset.dens) of sets of trials.

The agreement of a uniformly random trial is on average exactly 1 / 2 + (p₁ - p₀) / m, where p₁ and p₀ are the probabilities that the test accepts generated and uniform strings (Cslib.Crypto.PRG.NisanWigderson.expect_trialAgreement): at a fixed position, the average agreement is the probability that the predictor built from the test guesses that bit (Cslib.Crypto.PRG.NisanWigderson.toReal_predictionExperiment_eq_expect_trialAgreement), and the hybrid gaps telescope. Agreements are at most 1, so by reverse averaging (Fintype.expect_sub_le_dens_filter) a uniformly random trial has agreement at least 1 / 2 + ε / (2 m) with probability at least ε / (2 m) (Cslib.Crypto.PRG.NisanWigderson.div_two_mul_le_dens_goodTrials). Among k independent trials one does with probability at least 1 - (1 - ε / (2 m)) ^ k (Cslib.Crypto.PRG.NisanWigderson.one_sub_pow_le_dens_exists_mem_goodTrials), which is at least 1 / 2 once k ε ≥ 2 m, for instance for k = ⌈2 m / ε⌉ (Cslib.Crypto.PRG.NisanWigderson.half_le_dens_exists_mem_goodTrials).

Main definitions

• Cslib.Crypto.PRG.NisanWigderson.Trial: the random choices of the reconstruction.
• Cslib.Crypto.PRG.NisanWigderson.trialGuess: the guess of the predictor built from a deterministic test, with its random choices fixed.
• Cslib.Crypto.PRG.NisanWigderson.trialAgreement: the fraction of inputs on which it is correct.
• Cslib.Crypto.PRG.NisanWigderson.goodTrials: the trials whose agreement reaches a threshold.

Main results

• Cslib.Crypto.PRG.Generator.toReal_realExperiment_pure, Cslib.Crypto.PRG.Generator.toReal_idealExperiment_pure: the experiments of a deterministic test are densities.
• Cslib.Crypto.PRG.NisanWigderson.toReal_predictionExperiment_eq_expect_trialAgreement, Cslib.Crypto.PRG.NisanWigderson.expect_trialAgreement: the prediction experiments are averages of agreements.
• Cslib.Crypto.PRG.NisanWigderson.half_add_div_le_expect_trialAgreement, Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_trialAgreement: a test with advantage ε gives average agreement at least 1 / 2 + ε / m, so some trial reaches it.
• Cslib.Crypto.PRG.NisanWigderson.sub_div_le_dens_goodTrials, Cslib.Crypto.PRG.NisanWigderson.div_two_mul_le_dens_goodTrials: a random trial is good with probability at least ε / (2 m).
• Cslib.Crypto.PRG.NisanWigderson.one_sub_pow_le_dens_exists_mem_goodTrials, Cslib.Crypto.PRG.NisanWigderson.half_le_dens_exists_mem_goodTrials: repeated trials.

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, Chapter 20

theorem Cslib.Crypto.PRG.Generator.toReal_realExperiment_pure {Seed : Type u_1} {Output : Type u_2} [Fintype Seed] [Nonempty Seed] (G : Generator Seed Output) (test : Output → Bool) : ((G.realExperiment fun (y : Output) => PMF.pure (test y)) true).toReal = ↑{z : Seed | test (G z) = true}.dens

A deterministic test accepts the output of a generator on a uniform seed with probability the density of the seeds on which it accepts.

theorem Cslib.Crypto.PRG.Generator.toReal_idealExperiment_pure {Output : Type u_2} [Fintype Output] [Nonempty Output] (test : Output → Bool) : ((idealExperiment fun (y : Output) => PMF.pure (test y)) true).toReal = ↑{y : Output | test y = true}.dens

A deterministic test accepts a uniform string with probability the density of the strings it accepts.

structure Cslib.Crypto.PRG.NisanWigderson.Trial (ℓ m : ℕ) : Type

A trial of the reconstruction: its random choices. These are a position pos, a seed seed whose bits outside the pos-th block are kept, a candidate bit bit for the bit at pos, and a string pad whose bits after position pos pad the input of the test.

• pos : Fin m

  The position of the predicted bit.

• seed : Fin ℓ → Bool

  The seed; its bits outside the pos-th block are kept.

• bit : Bool

  The candidate value of the predicted bit.

• pad : Fin m → Bool

  The padding; its bits after position pos complete the input of the test.

def Cslib.Crypto.PRG.NisanWigderson.instDecidableEqTrial.decEq {ℓ✝ m✝ : ℕ} (x✝ x✝¹ : Trial ℓ✝ m✝) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Crypto.PRG.NisanWigderson.instDecidableEqTrial {ℓ✝ m✝ : ℕ} : DecidableEq (Trial ℓ✝ m✝)

@[instance_reducible]

instance Cslib.Crypto.PRG.NisanWigderson.instFintypeTrial {ℓ✝ m✝ : ℕ} : Fintype (Trial ℓ✝ m✝)

def Cslib.Crypto.PRG.NisanWigderson.Trial.equivProd {ℓ m : ℕ} : Trial ℓ m ≃ Fin m × (Fin ℓ → Bool) × Bool × (Fin m → Bool)

A trial is its four random choices.

instance Cslib.Crypto.PRG.NisanWigderson.instNonemptyTrialOfNeZeroNat {ℓ m : ℕ} [NeZero m] : Nonempty (Trial ℓ m)

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

The guess at the input x of the predictor built from the deterministic test test, with the random choices t fixed: nextBitGuess test t.pos t.bit t.pad applied to the first t.pos bits of the output of the generator on the seed D.extend t.pos x t.seed.

def Cslib.Crypto.PRG.NisanWigderson.trialAgreement {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (t : Trial ℓ m) : ℚ≥0

The agreement of the trial t: the fraction of the inputs x on which its guess is f x.

noncomputable def Cslib.Crypto.PRG.NisanWigderson.goodTrials {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (θ : ℝ) : Finset (Trial ℓ m)

The good trials at threshold θ: those with agreement at least θ.

@[simp]

theorem Cslib.Crypto.PRG.NisanWigderson.mem_goodTrials {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) {θ : ℝ} {t : Trial ℓ m} : t ∈ goodTrials D f test θ ↔ θ ≤ ↑(trialAgreement D f test t)

theorem Cslib.Crypto.PRG.NisanWigderson.trialAgreement_le_one {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (t : Trial ℓ m) : trialAgreement D f test t ≤ 1

An agreement is at most 1.

theorem Cslib.Crypto.PRG.NisanWigderson.toReal_predictionExperiment_eq_expect_trialAgreement {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (i : Fin m) : (((generator D f).predictionExperiment i (nextBitPredictor (fun (y : Fin m → Bool) => PMF.pure (test y)) i)) true).toReal = Finset.univ.expect fun (w : Fin ℓ → Bool) => Finset.univ.expect fun (r : Bool) => Finset.univ.expect fun (u : Fin m → Bool) => ↑(trialAgreement D f test { pos := i, seed := w, bit := r, pad := u })

Averaging over the random choices. For a deterministic test, the probability that the predictor built from it guesses bit i of the generator is the average agreement of the trials at position i.

theorem Cslib.Crypto.PRG.NisanWigderson.expect_trialAgreement {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (hm : 0 < m) : (Finset.univ.expect fun (t : Trial ℓ m) => ↑(trialAgreement D f test t)) = 1 / 2 + ((((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) / ↑m

Averaging over the random choices. If 0 < m, the agreement of a uniformly random trial is on average 1 / 2 + (p₁ - p₀) / m, where the test accepts generated strings with probability p₁ and uniform strings with probability p₀.

theorem Cslib.Crypto.PRG.NisanWigderson.half_add_div_le_expect_trialAgreement {ℓ 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) : 1 / 2 + ε / ↑m ≤ Finset.univ.expect fun (t : Trial ℓ m) => ↑(trialAgreement D f test t)

If 0 < m, a deterministic test that accepts generated strings with probability at least ε more than uniform ones gives an average agreement of at least 1 / 2 + ε / m.

theorem Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_trialAgreement {ℓ 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) : ∃ (t : Trial ℓ m), 1 / 2 + ε / ↑m ≤ ↑(trialAgreement D f test t)

The reconstruction, in the vocabulary of trials: if 0 < m and a deterministic test accepts generated strings with probability at least ε more than uniform ones, some trial has agreement at least 1 / 2 + ε / m.

theorem Cslib.Crypto.PRG.NisanWigderson.sub_div_le_dens_goodTrials {ℓ 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) {θ : ℝ} (hθ : θ < 1) : (1 / 2 + ε / ↑m - θ) / (1 - θ) ≤ ↑(goodTrials D f test θ).dens

Sampling the advice, exact form. Let 0 < m and let a deterministic test accept generated strings with probability at least ε more than uniform ones. For every θ < 1, a uniformly random trial has agreement at least θ with probability at least (1 / 2 + ε / m - θ) / (1 - θ).

theorem Cslib.Crypto.PRG.NisanWigderson.div_two_mul_le_dens_goodTrials {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (hm : 0 < m) {ε : ℝ} (hε₀ : 0 ≤ ε) (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) : ε / (2 * ↑m) ≤ ↑(goodTrials D f test (1 / 2 + ε / (2 * ↑m))).dens

Sampling the advice [Hir18]. Let 0 < m, 0 ≤ ε, and let a deterministic test accept generated strings with probability at least ε more than uniform ones. A uniformly random trial has agreement at least 1 / 2 + ε / (2 m) with probability at least ε / (2 m).

theorem Cslib.Crypto.PRG.NisanWigderson.one_sub_pow_le_dens_exists_mem_goodTrials {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (hm : 0 < m) {ε : ℝ} (hε₀ : 0 ≤ ε) (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) (k : ℕ) : 1 - (1 - ε / (2 * ↑m)) ^ k ≤ ↑{ts : Fin k → Trial ℓ m | ∃ (j : Fin k), ts j ∈ goodTrials D f test (1 / 2 + ε / (2 * ↑m))}.dens

Repeated sampling. Let 0 < m, 0 ≤ ε, and let a deterministic test accept generated strings with probability at least ε more than uniform ones. Among k independent uniformly random trials, one has agreement at least 1 / 2 + ε / (2 m) with probability at least 1 - (1 - ε / (2 m)) ^ k.

theorem Cslib.Crypto.PRG.NisanWigderson.half_le_dens_exists_mem_goodTrials {ℓ n a m : ℕ} (D : Design ℓ n a m) (f : (Fin n → Bool) → Bool) (test : (Fin m → Bool) → Bool) (hm : 0 < m) {ε : ℝ} (hε₀ : 0 ≤ ε) (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) {k : ℕ} (hk : 2 * ↑m ≤ ↑k * ε) : 1 / 2 ≤ ↑{ts : Fin k → Trial ℓ m | ∃ (j : Fin k), ts j ∈ goodTrials D f test (1 / 2 + ε / (2 * ↑m))}.dens

Repeated sampling [Hir18]. Let 0 < m, 0 ≤ ε, and let a deterministic test accept generated strings with probability at least ε more than uniform ones. If 2 m ≤ k ε, then among k independent uniformly random trials one has agreement at least 1 / 2 + ε / (2 m) with probability at least 1 / 2.