Impagliazzo's hard-core lemma

A measure on the inputs of a Boolean function f on n bits is a weight M x ∈ [0, 1] for each input; its density is its total mass divided by 2 ^ n. A function g agrees with f on a p fraction of the mass of M when ∑ x with g x = f x, M x = p ∑ x, M x. A hard-core measure of density δ for f against circuits of size s with advantage ε (IsHardCoreMeasure) is a measure of density at least δ on whose mass every Boolean function of De Morgan circuit complexity at most s agrees with f on at most a 1 / 2 + ε fraction.

Impagliazzo's hard-core lemma [Imp95] says that a function which every small circuit gets wrong on a δ fraction of the inputs has a hard-core measure of density δ on which somewhat smaller circuits barely beat a coin flip (exists_isHardCoreMeasure). Precisely, let T be a number of rounds with 3 ε² δ² T ≥ 1. If every function of complexity at most T s + 2 + 2 T (T + 2) agrees with f on at most a 1 - δ fraction of the inputs, then f has a hard-core measure of density δ against circuits of size s with advantage ε. So hardness for size S ≥ 2 + 2 T (T + 2) gives a hard-core measure against size (S - 2 - 2 T (T + 2)) / T (exists_isHardCoreMeasure_of_le): for T = ⌈1 / (3 ε² δ²)⌉ the size shrinks by a factor polynomial in 1 / ε and 1 / δ and by an additive O(T), independently of n.

The proof is Impagliazzo's boosting argument with the clipped linear weights of Cslib.Crypto.Pseudoentropy.Boosting.weight, at rate ε δ. If no hard-core measure exists, a small circuit g_j beats the measure M_j(x) = weight (ε δ) (N_j x) built from the margin N_j x = #{l < j | g_l x = f x} - #{l < j | g_l x ≠ f x} of the previous circuits, as long as M_j has density at least δ. Each such round gains at least 2 ε δ 2 ^ n in the correlation ∑ x, M_j x (±1), while the potential Cslib.Crypto.Pseudoentropy.Boosting.potential caps the total gain over T rounds at 2 ^ n (1 / (2 ε δ) + T ε δ / 2). So within T rounds some M_j has density less than δ; the strict majority of g_0, …, g_{j-1} is then correct on every input of positive margin, and the inputs of nonpositive margin have weight 1, so it errs on fewer than δ 2 ^ n inputs. The majority costs at most T s gates for the votes and 2 + 2 T (T + 2) for strict majority (Cslib.Circuits.Boolean.complexity_threshold_le).

Everything is nonuniform: the circuits are arbitrary De Morgan circuits, sizes are counted as in Cslib.Circuits.complexity, and nothing is claimed about constructing them.

Main definitions

• Cslib.Circuits.Boolean.IsHardCoreMeasure: a hard-core measure of density δ against circuits of size s with advantage ε.

Main results

• Cslib.Circuits.Boolean.exists_isHardCoreMeasure: Impagliazzo's hard-core lemma, with the size loss s ↦ T s + 2 + 2 T (T + 2) for any T with 3 ε² δ² T ≥ 1.
• Cslib.Circuits.Boolean.exists_isHardCoreMeasure_of_le: the same, from hardness for a given size S.

References

• R. Impagliazzo, Hard-core distributions for somewhat hard problems
• T. Holenstein, Key agreement from weak bit agreement, Section 2.2
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 19

structure Cslib.Circuits.Boolean.IsHardCoreMeasure {n : ℕ} (f : BooleanFunction n) (s : ℕ) (δ ε : ℝ) (M : BitString n → ℝ) : Prop

A hard-core measure M of density δ for f against circuits of size s with advantage ε [Imp95]: its weights lie in [0, 1], its total mass is at least δ 2 ^ n, and every Boolean function of De Morgan circuit complexity at most s agrees with f on at most a 1 / 2 + ε fraction of its mass.

• mem_Icc (x : BitString n) : M x ∈ Set.Icc 0 1

  Every weight is a probability.

• mul_two_pow_le_sum : δ * 2 ^ n ≤ ∑ x : BitString n, M x

  The measure has density at least δ.

• sum_agree_le (g : BooleanFunction n) : complexity interpretation (single g) ≤ s → ∑ x : BitString n with g x = f x, M x ≤ (1 / 2 + ε) * ∑ x : BitString n, M x

  Every function computed with at most s gates agrees with f on at most a 1 / 2 + ε fraction of the mass.

theorem Cslib.Circuits.Boolean.IsHardCoreMeasure.sum_le {n : ℕ} {f : BooleanFunction n} {s : ℕ} {δ ε : ℝ} {M : BitString n → ℝ} (hM : IsHardCoreMeasure f s δ ε M) : ∑ x : BitString n, M x ≤ 2 ^ n

The total mass of a measure is at most the number of inputs.

theorem Cslib.Circuits.Boolean.exists_isHardCoreMeasure {n : ℕ} {f : BooleanFunction n} {s T : ℕ} {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) (hT : 1 ≤ 3 * ε ^ 2 * δ ^ 2 * ↑T) (hf : ∀ (g : BooleanFunction n), complexity interpretation (single g) ≤ T * s + (2 + T * (2 * (T + 2))) → ↑{x : BitString n | g x = f x}.card / 2 ^ n ≤ 1 - δ) : ∃ (M : BitString n → ℝ), IsHardCoreMeasure f s δ ε M

Impagliazzo's hard-core lemma [Imp95], with explicit parameters. Let 0 < δ, 0 < ε, and let T be a number of rounds with 1 ≤ 3 ε² δ² T. If every Boolean function of De Morgan circuit complexity at most T s + (2 + T (2 (T + 2))) agrees with f on at most a 1 - δ fraction of the inputs, then f has a hard-core measure of density δ against circuits of size s with advantage ε: a measure M with weights in [0, 1] and mass at least δ 2 ^ n on whose mass every function of complexity at most s agrees with f on at most a 1 / 2 + ε fraction.

theorem Cslib.Circuits.Boolean.exists_isHardCoreMeasure_of_le {n : ℕ} {f : BooleanFunction n} {S T : ℕ} {δ ε : ℝ} (hδ : 0 < δ) (hε : 0 < ε) (hT : 1 ≤ 3 * ε ^ 2 * δ ^ 2 * ↑T) (hS : 2 + T * (2 * (T + 2)) ≤ S) (hf : ∀ (g : BooleanFunction n), complexity interpretation (single g) ≤ S → ↑{x : BitString n | g x = f x}.card / 2 ^ n ≤ 1 - δ) : ∃ (M : BitString n → ℝ), IsHardCoreMeasure f ((S - (2 + T * (2 * (T + 2)))) / T) δ ε M

Impagliazzo's hard-core lemma [Imp95] from hardness for a given size. Let 0 < δ, 0 < ε, let T be a number of rounds with 1 ≤ 3 ε² δ² T, and let 2 + T (2 (T + 2)) ≤ S. If every Boolean function of De Morgan circuit complexity at most S agrees with f on at most a 1 - δ fraction of the inputs, then f has a hard-core measure of density δ against circuits of size (S - (2 + T (2 (T + 2)))) / T with advantage ε.