Natural proofs

A property of Boolean functions is a set C n of functions on n inputs for each n. Razborov and Rudich call it natural when it contains a property D that is large, holding for at least a 2 ^ (-O(n)) fraction of all functions on n inputs, and constructive, decided from the truth table of length 2 ^ n within some class Γ of languages, for instance by circuits of size polynomial in 2 ^ n (Γ = P/poly) [RR97]. It is useful against a class Λ of languages when the slices of every language in Λ eventually lie outside it. A lower-bound proof against Λ exhibits a property useful against Λ, and Razborov and Rudich observe that the properties used by the known proofs are natural.

The natural proofs barrier. If a property holds for no function of a keyed family, the test deciding it from truth tables never accepts the truth table of a member, but accepts that of a uniformly random function with probability the density of the property (advantage_truthTableGenerator_truthTableTest). A property decided by circuits with t gates and useful against circuits with s gates therefore distinguishes every keyed family of functions with s gates from uniformly random functions, by a circuit with t gates and with advantage its density (not_secure_truthTableGenerator). Asymptotically, no P/poly-natural property is useful against P/poly if some keyed family with members of polynomial circuit size is exponentially secure, pseudorandom against circuits of size 2 ^ (c n) with error 2 ^ (-c n) for every c (Cslib.Crypto.PRG.IsExponentiallySecure, not_isUseful_PPoly_of_isNatural).

Razborov and Rudich obtain such a family from a pseudorandom generator secure against circuits of size 2 ^ (k ^ ε) on seeds of length k, by the construction of Goldreich, Goldwasser and Micali [GGM86] with keys of length polynomial in n. That derivation, with its circuit-size analysis, is Cslib.Crypto.GGM.isExponentiallySecure_booleanFamily, and the barrier from such a generator is Cslib.Circuits.Boolean.not_isUseful_PPoly_of_isNatural_of_generator (Complexity.Computability.Circuit.Boolean.NaturalProof.Generator).

Security is cslib's concrete security of generators (Cslib.Crypto.PRG.Generator.Secure), for the generator mapping a key to the truth table of its function (Cslib.Crypto.PRG.truthTableGenerator), against the deterministic tests computed by De Morgan circuits with at most t gates (Cslib.Crypto.PRG.IsCircuitTest). These tests read the whole truth table, that is they query the function at every input, as the distinguisher of Razborov and Rudich does. Circuit sizes count every AND, OR, NOT and constant gate.

The functions on n inputs that need more than 2 ^ n / (5 n) gates form a property that is large, by counting circuits, and useful against P/poly (isLarge_setOf_lt_complexity, isUseful_PPoly_setOf_lt_complexity). Under the same hypothesis it is therefore not P/poly-natural (not_isNatural_PPoly_setOf_lt_complexity), and not P/poly-constructive: its truth tables, the no-instances of GapMCSP at threshold 2 ^ n / (5 n), do not form a language in P/poly (truthTableLanguage_setOf_lt_complexity_notMem_PPoly) [KC00].

Main definitions

• Cslib.Circuits.Boolean.truthTableTest: the test deciding a property from truth tables.
• Cslib.Circuits.Boolean.truthTableLanguage: the truth tables of a property, as a language.
• Cslib.Circuits.Boolean.NaturalProof.IsLarge, Cslib.Circuits.Boolean.NaturalProof.IsNatural, Cslib.Circuits.Boolean.NaturalProof.IsUseful: large, natural and useful properties.

Main results

• Cslib.Circuits.Boolean.isUseful_PPoly_iff: usefulness against P/poly as a bound on the circuit complexity of every function with the property.
• Cslib.Circuits.Boolean.NaturalProof.IsNatural.PPoly_of_P: P-natural properties, decided in time polynomial in the length of the truth table, are P/poly-natural.
• Cslib.Circuits.Boolean.advantage_truthTableGenerator_truthTableTest: the advantage of the Razborov–Rudich distinguisher is the density of the property.
• Cslib.Circuits.Boolean.not_secure_truthTableGenerator: the barrier for one input length, with explicit sizes and advantage.
• Cslib.Circuits.Boolean.not_isUseful_PPoly_of_isNatural: the natural proofs barrier for P/poly, assuming an exponentially secure keyed family.
• Cslib.Circuits.Boolean.isLarge_setOf_lt_complexity, Cslib.Circuits.Boolean.isUseful_PPoly_setOf_lt_complexity: the functions needing more than 2 ^ n / (5 n) gates form a large property useful against P/poly.
• Cslib.Circuits.Boolean.not_isNatural_PPoly_setOf_lt_complexity, Cslib.Circuits.Boolean.truthTableLanguage_setOf_lt_complexity_notMem_PPoly: under the same assumption, this property is not P/poly-natural, and the truth tables of these hard functions do not form a language in P/poly.

References

• A. A. Razborov, S. Rudich, Natural proofs
• O. Goldreich, S. Goldwasser, S. Micali, How to construct random functions
• V. Kabanets, J.-Y. Cai, Circuit minimization problem

Properties of Boolean functions

noncomputable def Cslib.Circuits.Boolean.truthTableTest {n : ℕ} (C : Set (BooleanFunction n)) : BooleanFunction (2 ^ n)

The test that accepts the truth tables of the functions in C. Its circuit complexity is the size of the smallest circuits deciding C from truth tables.

@[simp]

theorem Cslib.Circuits.Boolean.truthTableTest_eq_true_iff {n : ℕ} {C : Set (BooleanFunction n)} {T : BitString (2 ^ n)} : truthTableTest C T = true ↔ (MCSP.truthTable n).symm T ∈ C

theorem Cslib.Circuits.Boolean.truthTableTest_truthTable_eq_true_iff {n : ℕ} {C : Set (BooleanFunction n)} {f : BooleanFunction n} : truthTableTest C ((MCSP.truthTable n) f) = true ↔ f ∈ C

theorem Cslib.Circuits.Boolean.card_filter_truthTableTest {n : ℕ} (C : Set (BooleanFunction n)) : {T : BitString (2 ^ n) | truthTableTest C T = true}.card = C.ncard

The test deciding C accepts as many truth tables as there are functions in C.

def Cslib.Circuits.Boolean.truthTableLanguage (C : (n : ℕ) → Set (BooleanFunction n)) : Language Bool

The truth tables of a property, as a language [RR97]: a word of length 2 ^ n belongs to it when it is the truth table of a function in C n. Words whose length is not a power of two do not belong to it.

theorem Cslib.Circuits.Boolean.ofFn_mem_truthTableLanguage {n : ℕ} {C : (n : ℕ) → Set (BooleanFunction n)} {T : BitString (2 ^ n)} : List.ofFn T ∈ truthTableLanguage C ↔ (MCSP.truthTable n).symm T ∈ C n

@[simp]

theorem Cslib.Circuits.Boolean.slice_truthTableLanguage (C : (n : ℕ) → Set (BooleanFunction n)) (n : ℕ) : (truthTableLanguage C).slice (2 ^ n) = truthTableTest (C n)

At length 2 ^ n, the truth-table language of C is decided by the test for C n.

def Cslib.Circuits.Boolean.NaturalProof.IsLarge (C : (n : ℕ) → Set (BooleanFunction n)) : Prop

Largeness [RR97]: for some c, eventually at least a 2 ^ (-c n) fraction of the 2 ^ 2 ^ n Boolean functions on n inputs lie in C n.

def Cslib.Circuits.Boolean.NaturalProof.IsNatural (Γ : Set (Language Bool)) (C : (n : ℕ) → Set (BooleanFunction n)) : Prop

Natural properties [RR97]: C is Γ-natural when it contains a large property whose truth tables form a language in Γ. For Γ = PPoly that property is decided by circuits of size polynomial in the length 2 ^ n of the truth table, that is of size 2 ^ O(n) (exists_complexity_truthTableTest_le).

def Cslib.Circuits.Boolean.NaturalProof.IsUseful (Λ : Set (Language Bool)) (C : (n : ℕ) → Set (BooleanFunction n)) : Prop

Usefulness [RR97]: C is useful against a class Λ of languages when the slices of every language in Λ eventually lie outside C. Against P/poly, this says that for every polynomial bound, eventually every function in C n needs more gates (isUseful_PPoly_iff).

theorem Cslib.Circuits.Boolean.NaturalProof.IsLarge.mono {C C' : (n : ℕ) → Set (BooleanFunction n)} (hC : IsLarge C) (h : ∀ (n : ℕ), C n ⊆ C' n) : IsLarge C'

theorem Cslib.Circuits.Boolean.NaturalProof.IsNatural.mono {Γ Γ' : Set (Language Bool)} {C C' : (n : ℕ) → Set (BooleanFunction n)} (hC : IsNatural Γ C) (hΓ : Γ ⊆ Γ') (h : ∀ (n : ℕ), C n ⊆ C' n) : IsNatural Γ' C'

A larger class of deciders, or a larger property, keeps a property natural.

theorem Cslib.Circuits.Boolean.NaturalProof.IsUseful.anti {Λ Λ' : Set (Language Bool)} {C C' : (n : ℕ) → Set (BooleanFunction n)} (hC : IsUseful Λ C) (hΛ : Λ' ⊆ Λ) (h : ∀ (n : ℕ), C' n ⊆ C n) : IsUseful Λ' C'

A smaller class, or a smaller property, keeps a property useful.

theorem Cslib.Circuits.Boolean.NaturalProof.IsUseful.eventually_lt_complexity {Λ : Set (Language Bool)} {C : (n : ℕ) → Set (BooleanFunction n)} (hC : IsUseful Λ C) {s : ℕ → ℕ} (hΛ : SIZE s ⊆ Λ) (hs : ∀ (n : ℕ), 1 ≤ s n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ f ∈ C n, s n < complexity interpretation (single f)

If Λ contains SIZE s, with s positive, a property useful against Λ eventually holds only for functions needing more than s n gates.

theorem Cslib.Circuits.Boolean.isUseful_PPoly_iff {C : (n : ℕ) → Set (BooleanFunction n)} : NaturalProof.IsUseful PPoly C ↔ ∀ (s : ℕ → ℕ), PolynomiallyBounded s → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ f ∈ C n, s n < complexity interpretation (single f)

Usefulness against P/poly, in the form of [RR97]: for every polynomially bounded s, eventually every function in C n needs more than s n gates.

theorem Cslib.Circuits.Boolean.exists_complexity_truthTableTest_le {C : (n : ℕ) → Set (BooleanFunction n)} (hC : truthTableLanguage C ∈ PPoly) : ∃ (c : ℕ), ∀ (n : ℕ), 1 ≤ n → complexity interpretation (single (truthTableTest (C n))) ≤ 2 ^ (c * n)

A P/poly-constructive property is decided by circuits of size 2 ^ O(n).

theorem Cslib.Circuits.Boolean.NaturalProof.IsNatural.PPoly_of_P {C : (n : ℕ) → Set (BooleanFunction n)} (hC : IsNatural {L : Language Bool | L ∈ Complexity.P Turing.MultiTapeTM.encBits} C) : IsNatural PPoly C

A property that is natural for the class P, applied to truth tables, is P/poly-natural: a problem decided in time polynomial in the length of the truth table has circuits of polynomial size (PPoly.of_mem_P).

The Razborov–Rudich distinguisher

theorem Cslib.Circuits.Boolean.advantage_truthTableGenerator_truthTableTest {n : ℕ} {Key : Type u_1} [Fintype Key] [Nonempty Key] (F : Key → BooleanFunction n) {C : Set (BooleanFunction n)} (hF : ∀ (key : Key), F key ∉ C) : ((Crypto.PRG.truthTableGenerator F).advantage fun (T : BitString (2 ^ n)) => PMF.pure (truthTableTest C T)) = ↑C.ncard / 2 ^ 2 ^ n

The Razborov–Rudich distinguisher [RazborovRudich1997, Section 4]. If no function of the keyed family F lies in C, the test deciding C from truth tables never accepts the truth table of F key, and accepts that of a uniformly random function with probability the density of C. Its advantage is therefore exactly the density of C.

theorem Cslib.Circuits.Boolean.not_secure_truthTableGenerator {n : ℕ} {Key : Type u_1} [Fintype Key] [Nonempty Key] {F : Key → BooleanFunction n} {C : Set (BooleanFunction n)} {s t : ℕ} {ε : NNReal} (hconstructive : complexity interpretation (single (truthTableTest C)) ≤ t) (huseful : ∀ f ∈ C, s < complexity interpretation (single f)) (hF : ∀ (key : Key), complexity interpretation (single (F key)) ≤ s) (hε : ↑ε < ↑C.ncard / 2 ^ 2 ^ n) : ¬(Crypto.PRG.truthTableGenerator F).Secure (Crypto.PRG.IsCircuitTest t) ε

Natural properties break pseudorandom function families, for one input length [RazborovRudich1997, Section 4]. Let C be a property of functions on n inputs that is decided from truth tables by circuits with at most t gates and holds for no function computable with at most s gates. Then no keyed family of functions computable with at most s gates is pseudorandom against circuits with at most t gates with error below the density of C.

theorem Cslib.Circuits.Boolean.not_isUseful_PPoly_of_isNatural {C : (n : ℕ) → Set (BooleanFunction n)} {Key : ℕ → Type u_1} [(n : ℕ) → Fintype (Key n)] [∀ (n : ℕ), Nonempty (Key n)] {F : (n : ℕ) → Key n → BooleanFunction n} {s : ℕ → ℕ} (hs : PolynomiallyBounded s) (hF : ∀ (n : ℕ) (key : Key n), complexity interpretation (single (F n key)) ≤ s n) (hsecure : Crypto.PRG.IsExponentiallySecure F) (hC : NaturalProof.IsNatural PPoly C) : ¬NaturalProof.IsUseful PPoly C

The natural proofs barrier for P/poly [RazborovRudich1997, Section 4]. Suppose that for each n a keyed family F n of Boolean functions on n inputs has members with at most s n gates, for a polynomially bounded s, and is exponentially secure: for every c, eventually no circuit with at most 2 ^ (c n) gates distinguishes the truth table of a member with a uniformly random key from a uniformly random truth table with advantage more than 2 ^ (-c n). Then no P/poly-natural property is useful against P/poly.

Razborov and Rudich derive such a family from a pseudorandom generator secure against circuits of size 2 ^ (k ^ ε) by the construction of Goldreich, Goldwasser and Micali with keys of length polynomial in n: Cslib.Circuits.Boolean.not_isUseful_PPoly_of_isNatural_of_generator.

Hard functions

theorem Cslib.Circuits.Boolean.two_pow_two_pow_le_two_mul_ncard_setOf_lt_complexity {n : ℕ} (hn : 16 ≤ n) : 2 ^ 2 ^ n ≤ 2 * {f : BooleanFunction n | 2 ^ n / (5 * n) < complexity interpretation (single f)}.ncard

For n ≥ 16, at least half of the functions on n inputs need more than 2 ^ n / (5 n) gates, by counting circuits (MCSP.ncard_setOf_mem_le).

theorem Cslib.Circuits.Boolean.isLarge_setOf_lt_complexity : NaturalProof.IsLarge fun (n : ℕ) => {f : BooleanFunction n | 2 ^ n / (5 * n) < complexity interpretation (single f)}

The functions on n inputs that need more than 2 ^ n / (5 n) gates form a large property: for n ≥ 16 they are at least half of all functions.

theorem Cslib.Circuits.Boolean.isUseful_PPoly_setOf_lt_complexity : NaturalProof.IsUseful PPoly fun (n : ℕ) => {f : BooleanFunction n | 2 ^ n / (5 * n) < complexity interpretation (single f)}

Circuits of polynomial size eventually compute no function that needs more than 2 ^ n / (5 n) gates.

theorem Cslib.Circuits.Boolean.truthTableLanguage_setOf_lt_complexity_notMem_PPoly {Key : ℕ → Type u_1} [(n : ℕ) → Fintype (Key n)] [∀ (n : ℕ), Nonempty (Key n)] {F : (n : ℕ) → Key n → BooleanFunction n} {s : ℕ → ℕ} (hs : PolynomiallyBounded s) (hF : ∀ (n : ℕ) (key : Key n), complexity interpretation (single (F n key)) ≤ s n) (hsecure : Crypto.PRG.IsExponentiallySecure F) : (truthTableLanguage fun (n : ℕ) => {f : BooleanFunction n | 2 ^ n / (5 * n) < complexity interpretation (single f)}) ∉ PPoly

Under the hypothesis of not_isUseful_PPoly_of_isNatural, the truth tables of the functions on n inputs that need more than 2 ^ n / (5 n) gates, that is the no-instances GapMCSP.no (fun n => 2 ^ n / (5 * n)) n, do not form a language in P/poly [RR97], [KC00]. The property is large and useful against P/poly, so it is not P/poly-constructive.

theorem Cslib.Circuits.Boolean.not_isNatural_PPoly_setOf_lt_complexity {Key : ℕ → Type u_1} [(n : ℕ) → Fintype (Key n)] [∀ (n : ℕ), Nonempty (Key n)] {F : (n : ℕ) → Key n → BooleanFunction n} {s : ℕ → ℕ} (hs : PolynomiallyBounded s) (hF : ∀ (n : ℕ) (key : Key n), complexity interpretation (single (F n key)) ≤ s n) (hsecure : Crypto.PRG.IsExponentiallySecure F) : ¬NaturalProof.IsNatural PPoly fun (n : ℕ) => {f : BooleanFunction n | 2 ^ n / (5 * n) < complexity interpretation (single f)}

Under the hypothesis of not_isUseful_PPoly_of_isNatural, the property of needing more than 2 ^ n / (5 n) gates is not P/poly-natural: it is useful against P/poly [RR97].