Nonuniform Goldreich–Levin decoding

Goldreich–Levin decoding [GL89] recovers a string x from a predictor for its parities x ⬝ r with agreement 1 / 2 + ε, with probability at least 1 / 2 over random masks and for one of 2 ^ k guesses (Cslib.Crypto.GoldreichLevin.decode_failure_le_half). This module turns that into a statement about fixed choices, as needed for nonuniform reconstruction: for a family of predictors pred x with targets target x, if a set good of indices has agreement at least 1 / 2 + ε, then one fixed choice of masks and of the guess makes the corrected-majority candidate equal to the target for at least #good / 2 ^ (k + 1) of the indices (Cslib.Crypto.GoldreichLevin.exists_card_candidate_eq). The proof averages the success probability over the masks and over a uniformly random guess.

Main results

• Cslib.Crypto.GoldreichLevin.agreement_eq_card_div: agreement as a count.
• Cslib.Crypto.GoldreichLevin.card_le_two_mul_card_filter_mem_candidates: the counting form of the decoding guarantee.
• Cslib.Crypto.GoldreichLevin.exists_card_candidate_eq: fixed masks and guess recover a 1 / 2 ^ (k + 1) fraction of the good targets.

References

• O. Goldreich, L. Levin, A Hard-Core Predicate for All One-Way Functions

theorem Cslib.Crypto.GoldreichLevin.agreement_eq_card_div {n : ℕ} (predictor : BitString n → Bool) (x : BitString n) : agreement predictor x = ↑{r : BitString n | predictor r = x ⬝ᵥ r}.card / 2 ^ n

Agreement as a count: the fraction of queries on which the predictor is right.

theorem Cslib.Crypto.GoldreichLevin.card_le_two_mul_card_filter_mem_candidates {n k : ℕ} (predictor : BitString n → Bool) (x : BitString n) (ε : ℝ) (hε : 0 < ε) (hk : 0 < k) (h : 1 / 2 + ε ≤ agreement predictor x) (hsize : ↑n ≤ 2 * ε ^ 2 * ↑(2 ^ k - 1)) : Fintype.card (Fin k → BitString n) ≤ 2 * {masks : Fin k → BitString n | x ∈ candidates predictor masks}.card

The decoding guarantee in counting form. If a predictor agrees with the parities of x on a 1 / 2 + ε fraction of queries and n ≤ 2 * ε ^ 2 * (2 ^ k - 1), then x is a candidate for at least half of the choices of the k masks.

theorem Cslib.Crypto.GoldreichLevin.exists_card_candidate_eq {n k : ℕ} {X : Type u_1} [Fintype X] (pred : X → BitString n → Bool) (target : X → BitString n) (ε : ℝ) (hε : 0 < ε) (hk : 0 < k) (hsize : ↑n ≤ 2 * ε ^ 2 * ↑(2 ^ k - 1)) (good : Finset X) (hgood : ∀ x ∈ good, 1 / 2 + ε ≤ agreement (pred x) (target x)) : ∃ (masks : Fin k → BitString n) (guess : BitString k), good.card ≤ 2 ^ (k + 1) * {x : X | candidate (pred x) masks guess = target x}.card

Nonuniform Goldreich–Levin decoding. Let pred x be predictors for the parities of target x, indexed by a finite type, and let every index of good have agreement at least 1 / 2 + ε, with n ≤ 2 * ε ^ 2 * (2 ^ k - 1) and k ≥ 1. Then for some fixed masks and guess the corrected-majority candidate equals the target for at least #good / 2 ^ (k + 1) indices.