Short descriptions from distinguishers of the Nisan–Wigderson generator

Let C be a list code whose codewords are Boolean functions on n bits, and let a deterministic test distinguish the Nisan–Wigderson generator built from a design D and the codeword C.encode x of a message x. The reconstruction turns the test into a predictor of the codeword with advantage ε / m (Cslib.Crypto.PRG.NisanWigderson.exists_half_add_div_le_trialAgreement), determined by a reconstruction of at most m 2 ^ a bits (Cslib.Crypto.PRG.NisanWigderson.Reconstruction, Cslib.Crypto.PRG.NisanWigderson.reconstructionBits_le), and list decoding the predictor lists x among L candidates. So x is determined by the reconstruction and an index of ⌈log₂ L⌉ bits, given D, C and the test. This is the step from distinguishers to short time-bounded descriptions in Hirahara's analysis of the time-bounded Kolmogorov complexity problem [Hir18].

To turn this into a bound on the time-bounded complexity C_M^t(x) of a description method M, M must be able to run the decoder: from a description of the reconstruction and the index, output the candidate within t steps. No machine for the decoder is constructed in this library yet, so this is a hypothesis, Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder, in the style of Cslib.Kolmogorov.DescriptionMethod.Simulation: a compiler from reconstructions and indices to M-programs, with an explicit program overhead c over the length of a direct binary description and an explicit time bound t. Under it, C_M^t(x) ≤ m 2 ^ a + ⌈log₂ m⌉ + ⌈log₂ L⌉ + c (Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le). A test that accepts a δ fraction of all strings and no output of the generator has advantage δ, which gives the same bound for strings with a dense distinguisher (Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le_of_dens), in particular for a dense test that accepts only strings of high time-bounded complexity when all outputs of the generator have low time-bounded complexity (Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le_of_random).

Main definitions

• Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder: a description method that runs the decoder of the reconstruction, with explicit program and time overheads.

Main results

• Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le: a distinguisher of the generator built from the codeword of x gives a short time-bounded description of x.
• Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le_of_dens, Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le_of_random: the same from a dense test that avoids the outputs of the generator.

References

• S. Hirahara, Non-black-box worst-case to average-case reductions within NP
• N. Nisan, A. Wigderson, Hardness vs randomness
• M. Li, P. Vitányi, An Introduction to Kolmogorov Complexity and Its Applications

structure Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder {α : Type u_1} {ℓ n a m L : ℕ} (M : DescriptionMethod α) (D : Crypto.PRG.NisanWigderson.Design ℓ n a m) (C : ListCode α (Fin n → Bool) Bool L) (test : (Fin m → Bool) → Bool) (c t : ℕ) : Type

A reconstruction decoder in the description method M, for the design D, the list code C and the deterministic test test, with program overhead c and time bound t: every reconstruction R for D and every index k of the list decoder are compiled into an M-program that outputs, within t steps, the k-th candidate that C decodes from the guess of R, and whose length exceeds by at most c the ⌈log₂ m⌉ + reconstructionBits D R.pos + ⌈log₂ L⌉ bits of a direct binary description of R and k: the position in ⌈log₂ m⌉ bits, then the table entries, the padding and candidate bits, whose number reconstructionBits D R.pos is fixed by D and the position, and finally the index in ⌈log₂ L⌉ bits. Such descriptions are uniquely decodable once D and L are known.

This is all that is assumed of M to bound time-bounded complexities through the reconstruction: that it runs the decoder, with D, C and test built in, on direct descriptions of the decoder's input. The overhead c and the time bound t may depend on D, C and test, so the resulting bounds are relative to them; nothing is assumed about how the decoder evaluates the test or the list decoder, whose cost is part of t.

• program : Crypto.PRG.NisanWigderson.Reconstruction D → Fin L → List Bool

  The program describing the k-th candidate decoded from the reconstruction R.

• length_program_le (R : Crypto.PRG.NisanWigderson.Reconstruction D) (k : Fin L) : (self.program R k).length ≤ Nat.clog 2 m + Crypto.PRG.NisanWigderson.reconstructionBits D R.pos + Nat.clog 2 L + c

  A program exceeds a direct description of its reconstruction and index by at most c bits.

• mem_runFor_program (R : Crypto.PRG.NisanWigderson.Reconstruction D) (k : Fin L) : C.decode (R.guess test) k ∈ (M.run (self.program R k)).runFor t

  A program outputs its candidate within t steps.

theorem Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le {α : Type u_1} {ℓ n a m L : ℕ} {M : DescriptionMethod α} {D : Crypto.PRG.NisanWigderson.Design ℓ n a m} {C : ListCode α (Fin n → Bool) Bool L} {test : (Fin m → Bool) → Bool} {c t : ℕ} (I : M.ReconstructionDecoder D C test c t) (hm : 0 < m) {ε : ℝ} (hC : C.ListDecodes (1 / 2 - ε / ↑m)) {x : α} (hε : ε ≤ (((Crypto.PRG.NisanWigderson.generator D (C.encode x)).realExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal - ((Crypto.PRG.Generator.idealExperiment fun (y : Fin m → Bool) => PMF.pure (test y)) true).toReal) : M.etimeBoundedComplexity t x ≤ ↑(m * 2 ^ a + Nat.clog 2 m + Nat.clog 2 L + c)

Short descriptions from distinguishers [Hir18]. Let 0 < m, let the list code C list decode up to radius 1 / 2 - ε / m, and let M run the decoder of the reconstruction for the deterministic test test with program overhead c within t steps. If test accepts the outputs of the Nisan–Wigderson generator built from the codeword of x with probability at least ε more than uniform strings, then C_M^t(x) ≤ m 2 ^ a + ⌈log₂ m⌉ + ⌈log₂ L⌉ + c.

theorem Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le_of_dens {α : Type u_1} {ℓ n a m L : ℕ} {M : DescriptionMethod α} {D : Crypto.PRG.NisanWigderson.Design ℓ n a m} {C : ListCode α (Fin n → Bool) Bool L} {test : (Fin m → Bool) → Bool} {c t : ℕ} (I : M.ReconstructionDecoder D C (fun (y : Fin m → Bool) => !test y) c t) (hm : 0 < m) {δ : ℝ} (hC : C.ListDecodes (1 / 2 - δ / ↑m)) {x : α} (hδ : δ ≤ ↑{y : Fin m → Bool | test y = true}.dens) (havoid : ∀ (z : Fin ℓ → Bool), test ((Crypto.PRG.NisanWigderson.generator D (C.encode x)) z) = false) : M.etimeBoundedComplexity t x ≤ ↑(m * 2 ^ a + Nat.clog 2 m + Nat.clog 2 L + c)

Short descriptions from dense distinguishers [Hir18]. Let 0 < m, let the list code C list decode up to radius 1 / 2 - δ / m, and let M run the decoder of the reconstruction for the negation of the deterministic test test with program overhead c within t steps. If test accepts at least a δ fraction of all strings but no output of the Nisan–Wigderson generator built from the codeword of x, then C_M^t(x) ≤ m 2 ^ a + ⌈log₂ m⌉ + ⌈log₂ L⌉ + c.

theorem Cslib.Kolmogorov.DescriptionMethod.ReconstructionDecoder.etimeBoundedComplexity_le_of_random {α : Type u_1} {ℓ n a m L : ℕ} {M : DescriptionMethod α} {D : Crypto.PRG.NisanWigderson.Design ℓ n a m} {C : ListCode α (Fin n → Bool) Bool L} {test : (Fin m → Bool) → Bool} {c t : ℕ} (I : M.ReconstructionDecoder D C (fun (y : Fin m → Bool) => !test y) c t) (hm : 0 < m) {δ : ℝ} (hC : C.ListDecodes (1 / 2 - δ / ↑m)) {N : DescriptionMethod (Fin m → Bool)} {t' s : ℕ} (hδ : δ ≤ ↑{y : Fin m → Bool | test y = true}.dens) (hrandom : ∀ (y : Fin m → Bool), test y = true → ↑s ≤ N.etimeBoundedComplexity t' y) {x : α} (hlow : ∀ (z : Fin ℓ → Bool), N.etimeBoundedComplexity t' ((Crypto.PRG.NisanWigderson.generator D (C.encode x)) z) < ↑s) : M.etimeBoundedComplexity t x ≤ ↑(m * 2 ^ a + Nat.clog 2 m + Nat.clog 2 L + c)

Short descriptions from tests for random strings [Hir18]. Let N be a description method for m-bit strings, and let the deterministic test test accept at least a δ fraction of all strings, all of them of complexity C_N^{t'} ≥ s. Let 0 < m, let the list code C list decode up to radius 1 / 2 - δ / m, and let M run the decoder of the reconstruction for the negation of test with program overhead c within t steps. If every output of the Nisan–Wigderson generator built from the codeword of x has complexity C_N^{t'} < s, then C_M^t(x) ≤ m 2 ^ a + ⌈log₂ m⌉ + ⌈log₂ L⌉ + c.