Finite Goldreich–Levin decoding

The decoder samples k uniform base masks, forms their nonempty subset sums, and enumerates the 2 ^ k guesses for their inner products with the unknown string. Each guess gives one candidate, by correcting the predictor's answers and taking a majority for each coordinate.

The bitstrings are CSLib's Fin n → Bool. Mathlib's Boolean ring uses XOR for addition and AND for multiplication, so its ordinary dot product x ⬝ᵥ r is the required parity. Bilinearity, pairwise independence of subset sums, and Chebyshev's inequality give an explicit failure bound of n / (4 * ε ^ 2 * (2 ^ k - 1)) for a predictor of agreement at least 1 / 2 + ε. Taking 2 ^ k - 1 ≥ n / (2 * ε ^ 2) makes the failure probability at most one half.

This direct-coordinate variant has a larger candidate list than the sharper decoder in the reference, but the list remains polynomial in n and 1 / ε when k is chosen accordingly. It avoids a separate high-agreement decoder.

These theorems concern a deterministic predictor and finite probability distributions. The uniform PPT implementation and the hard-core reduction are separate steps. This module is adapted from the cslib crypto branch at 5ff69ca.

Main definitions

• nonemptySubsets, candidate, candidates: subset masks and candidate generation.
• agreement: the predictor's agreement with a parity function.
• decode: the finite distribution of candidate sets.

Main results

• decode_failure_le: the quantitative decoding guarantee.
• decode_failure_le_half: sufficient mask count gives success probability at least one half.
• candidate_parity: a perfect parity predictor recovers the target for every choice of masks.
• card_le_of_mem_support_decode: the candidate list has at most 2 ^ k elements.

References

• O. Goldreich, L. Levin, A Hard-Core Predicate for All One-Way Functions
• L. Trevisan, CS276 Lecture 12: Goldreich–Levin. We use the subset-sum construction and pairwise-independent majority estimate, adapting recovery to each coordinate.

def Cslib.Crypto.GoldreichLevin.nonemptySubsets (k : ℕ) : Finset (Finset (Fin k))

The nonempty subsets indexing the decoder's pairwise independent masks.

@[simp]

theorem Cslib.Crypto.GoldreichLevin.mem_nonemptySubsets {k : ℕ} (s : Finset (Fin k)) : s ∈ nonemptySubsets k ↔ s.Nonempty

Every voting subset is nonempty.

@[simp]

theorem Cslib.Crypto.GoldreichLevin.card_nonemptySubsets (k : ℕ) : (nonemptySubsets k).card = 2 ^ k - 1

There are 2 ^ k - 1 voting subsets of k base masks.

def Cslib.Crypto.GoldreichLevin.vote {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) (guess : BitString k) (i : Fin n) (s : Finset (Fin k)) : Bool

Predict one coordinate using a subset mask and the guessed parities of the base masks.

def Cslib.Crypto.GoldreichLevin.candidate {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) (guess : BitString k) : BitString n

One candidate string for a particular guess of the k base-mask parities.

def Cslib.Crypto.GoldreichLevin.candidates {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) : Finset (BitString n)

Enumerate all guesses of the base-mask parities and retain their candidate strings.

theorem Cslib.Crypto.GoldreichLevin.card_candidates_le {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) : (candidates predictor masks).card ≤ 2 ^ k

Enumerating k guessed bits produces at most 2 ^ k candidates.

theorem Cslib.Crypto.GoldreichLevin.vote_correct_iff {n k : ℕ} (predictor : BitString n → Bool) (masks : Fin k → BitString n) (x : BitString n) (i : Fin n) (s : Finset (Fin k)) : vote predictor masks (fun (j : Fin k) => x ⬝ᵥ masks j) i s = x i ↔ predictor (Pi.single i 1 + ∑ j ∈ s, masks j) = x ⬝ᵥ (Pi.single i 1 + ∑ j ∈ s, masks j)

With the true base-mask parities, a corrected vote is right exactly when the predictor is right on the shifted query. This is bilinearity of the Boolean dot product.

def Cslib.Crypto.GoldreichLevin.score {n : ℕ} (predictor : BitString n → Bool) (x r : BitString n) : ℝ

The real-valued indicator that a predictor agrees with the parity of x on r.

noncomputable def Cslib.Crypto.GoldreichLevin.agreement {n : ℕ} (predictor : BitString n → Bool) (x : BitString n) : ℝ

Agreement with a parity function, averaged over a uniform query.

noncomputable def Cslib.Crypto.GoldreichLevin.decode {n : ℕ} (predictor : BitString n → Bool) (k : ℕ) : PMF (Finset (BitString n))

Sample the base masks uniformly and return all candidates. This is a distributional specification; no machine-runtime certificate is asserted here.

theorem Cslib.Crypto.GoldreichLevin.decode_failure_le {n k : ℕ} (predictor : BitString n → Bool) (x : BitString n) (ε : ℝ) (hε : 0 < ε) (hk : 0 < k) (h : 1 / 2 + ε ≤ agreement predictor x) : (decode predictor k).toOuterMeasure {list : Finset (BitString n) | x ∉ list} ≤ ENNReal.ofReal (↑n / (4 * ε ^ 2 * ↑(2 ^ k - 1)))

The decoder misses a parity correlated with its predictor with probability at most n / (4 * ε ^ 2 * (2 ^ k - 1)). A union bound suffices across coordinates.

theorem Cslib.Crypto.GoldreichLevin.decode_failure_le_half {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)) : (decode predictor k).toOuterMeasure {list : Finset (BitString n) | x ∉ list} ≤ 1 / 2

With sufficiently many subset masks, the candidate list contains the target with probability at least one half.

theorem Cslib.Crypto.GoldreichLevin.candidate_parity {n k : ℕ} (x : BitString n) (masks : Fin k → BitString n) (hk : 0 < k) : (candidate (fun (r : BitString n) => x ⬝ᵥ r) masks fun (j : Fin k) => x ⬝ᵥ masks j) = x

For a perfect predictor, the true guessed parities recover the target for every choice of base masks, including repeated or zero masks.

theorem Cslib.Crypto.GoldreichLevin.mem_candidates_parity {n k : ℕ} (x : BitString n) (masks : Fin k → BitString n) (hk : 0 < k) : x ∈ candidates (fun (r : BitString n) => x ⬝ᵥ r) masks

Every run against a perfect parity predictor includes that parity's defining string.

theorem Cslib.Crypto.GoldreichLevin.agreement_eq_probability {n : ℕ} (predictor : BitString n → Bool) (x : BitString n) : agreement predictor x = ((PMF.map (fun (r : BitString n) => predictor r == x ⬝ᵥ r) (Probability.PMF.uniformOfFintype (BitString n))) true).toReal

Agreement is exactly the success probability of predicting the Boolean inner product.

theorem Cslib.Crypto.GoldreichLevin.agreement_le_one {n : ℕ} (predictor : BitString n → Bool) (x : BitString n) : agreement predictor x ≤ 1

Agreement with any fixed parity is a probability, hence at most one.

theorem Cslib.Crypto.GoldreichLevin.card_le_of_mem_support_decode {n k : ℕ} (predictor : BitString n → Bool) {list : Finset (BitString n)} (h : list ∈ (decode predictor k).support) : list.card ≤ 2 ^ k

Every possible output of the decoder has at most 2 ^ k candidates.