Yao's XOR lemma

The k-fold XOR of a Boolean function f on n bits is the function f^{⊕k}(x_1, …, x_k) = f(x_1) ⊕ ⋯ ⊕ f(x_k) on k blocks of n bits (xorPower). Yao's XOR lemma [Yao82] says that XOR amplifies hardness: if every small circuit errs on a δ fraction of the inputs of f, then somewhat smaller circuits agree with f^{⊕k} on at most a 1 / 2 + ε + (1 - δ) ^ k fraction of its inputs.

We derive it from Impagliazzo's hard-core lemma (Cslib.Circuits.Boolean.exists_isHardCoreMeasure) as in [Imp95]. Write each input weight as 1 = M x + (1 - M x) for a hard-core measure M of density δ. Expanding the first block, the part weighted by M is a prediction of f on the mass of M by a circuit with the other blocks fixed, which agrees with f on at most a 1 / 2 + ε fraction; the part weighted by 1 - M has mass at most (1 - δ) 2 ^ n and is handled by induction on the remaining blocks. This purely combinatorial step holds for any function all of whose single-block restrictions are hard on M, over any finite set of inputs (card_eq_sum_le): the agreement is at most (1 / 2 + ε) N ^ k + (1 / 2 - ε) (N - μ) ^ k for N inputs and a measure of mass μ. Fixing all blocks but one costs two gates for the constants (Cslib.Circuits.Boolean.complexity_substitute_le) and complementing costs one, so a hard-core measure against size s + 3 controls all circuits of size s (card_eq_xorPower_div_le).

Everything is nonuniform, over De Morgan circuits with sizes as in Cslib.Circuits.complexity.

Main definitions

• Cslib.Circuits.Boolean.xorPower: the k-fold XOR f^{⊕k} of a Boolean function.

Main results

• Cslib.Circuits.Boolean.card_eq_sum_le: the XOR lemma for a measure, over any finite set.
• Cslib.Circuits.Boolean.IsHardCoreMeasure.card_eq_xorPower_div_le: a hard-core measure of density δ against size s + 3 bounds the agreement of circuits of size s with f^{⊕k} by 1 / 2 + ε + (1 / 2 - ε) (1 - δ) ^ k.
• Cslib.Circuits.Boolean.card_eq_xorPower_div_le: Yao's XOR lemma with explicit parameters.

References

• A. C. Yao, Theory and applications of trapdoor functions
• R. Impagliazzo, Hard-core distributions for somewhat hard problems
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 19

def Cslib.Circuits.Boolean.xorPower {n : ℕ} (f : BooleanFunction n) (k : ℕ) : BooleanFunction (k * n)

The k-fold XOR f^{⊕k} of a Boolean function f on n bits: on k blocks of n bits (Cslib.BitString.block), the parity of the values of f on the blocks.

theorem Cslib.Circuits.Boolean.xorPower_apply {n : ℕ} (f : BooleanFunction n) (k : ℕ) (x : BitString (k * n)) : xorPower f k x = ∑ i : Fin k, f (x.block i)

The k-fold XOR is the sum of the values on the blocks in the Boolean ring Bool.

theorem Cslib.Circuits.Boolean.card_eq_sum_le {X : Type u_1} [Fintype X] (f : X → Bool) {M : X → ℝ} (hM : ∀ (x : X), M x ∈ Set.Icc 0 1) {ε : ℝ} (k : ℕ) (G : (Fin k → X) → Bool) : (∀ (i : Fin k) (t : Fin k → X) (b : Bool), ∑ y : X with (G (Function.update t i y) ^^ b) = f y, M y ≤ (1 / 2 + ε) * ∑ y : X, M y) → ↑{t : Fin k → X | G t = ∑ i : Fin k, f (t i)}.card ≤ (1 / 2 + ε) * ↑(Fintype.card X) ^ k + (1 / 2 - ε) * (↑(Fintype.card X) - ∑ y : X, M y) ^ k

The XOR lemma for a measure. Let M be a measure with weights in [0, 1] on a finite set X of N inputs, with mass μ, and let G be a function of k inputs all of whose single-input restrictions, complemented or not, agree with f on at most a 1 / 2 + ε fraction of the mass of M. Then G agrees with f(x_1) ⊕ ⋯ ⊕ f(x_k) on at most (1 / 2 + ε) N ^ k + (1 / 2 - ε) (N - μ) ^ k of the N ^ k tuples.

theorem Cslib.Circuits.Boolean.IsHardCoreMeasure.card_eq_xorPower_div_le {n : ℕ} {f : BooleanFunction n} {s : ℕ} {δ ε : ℝ} {M : BitString n → ℝ} (hM : IsHardCoreMeasure f (s + 3) δ ε M) (hε : ε ≤ 1 / 2) (k : ℕ) {g : BooleanFunction (k * n)} (hg : complexity interpretation (single g) ≤ s) : ↑{x : BitString (k * n) | g x = xorPower f k x}.card / 2 ^ (k * n) ≤ 1 / 2 + ε + (1 / 2 - ε) * (1 - δ) ^ k

A hard-core measure makes the XOR hard. If M is a hard-core measure of density δ for f against circuits of size s + 3 with advantage ε ≤ 1 / 2, then every Boolean function of De Morgan circuit complexity at most s agrees with the k-fold XOR f^{⊕k} on at most a 1 / 2 + ε + (1 / 2 - ε) (1 - δ) ^ k fraction of its inputs.

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

Yao's XOR lemma [Yao82], derived from Impagliazzo's hard-core lemma [Imp95], with explicit parameters. Let 0 < δ, 0 < ε ≤ 1 / 2, 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 + 3) + (2 + T (2 (T + 2))) agrees with f on at most a 1 - δ fraction of the inputs, then every Boolean function of complexity at most s agrees with the k-fold XOR f^{⊕k} on at most a 1 / 2 + ε + (1 / 2 - ε) (1 - δ) ^ k fraction of its inputs.