Polynomial-time word algorithms for Goldreich–Levin decoding

The decoder is ordinary functional code: maps, filtering, folds and first-match search. Its deterministic certificates use the shared tidy TM calculus. A fixed precision degree keeps both the number of guesses and their complete encoded size polynomially bounded. Exact representation laws preserve candidate order, duplicates, the fallback and every mask tape.

The predictor may capture public data and saved coins. Its certificate must be uniform jointly in that environment and its query. Sampling and uniform PPT adversaries are connected in the subsequent reduction; this module certifies the deterministic decoder.

Main definitions

• wordCandidate, wordCandidates: corrected majority voting for each parity guess.
• wordCheckCandidates: select the first preimage, with a zero-word fallback.
• wordDecode: decode and check all guesses from one mask tape.

Main results

• polyTime_wordDecode: uniform deterministic polynomial time for any efficient captured predictor.
• wordDecode_eq_ofFn, uniform_wordDecode: exact finite-algorithm and distributional agreement.
• wordDecode_success_ge_half: correlated prediction gives a valid preimage with probability at least one half.

References

• O. Goldreich, L. Levin, A Hard-Core Predicate for All One-Way Functions
• L. Trevisan, CS276 Lecture 12: Goldreich–Levin

Adapted from Crypto/Computational/GoldreichLevin/WordDecoder.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Crypto.GoldreichLevin.polyTime_precision {α : Type} {input : α ↪ List Bool} {parameter : α → ℕ} (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter input Turing.MultiTapeTM.encUnary) (degree : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => precision degree (parameter a)) input Turing.MultiTapeTM.encUnary

A fixed precision degree is computable from a unary security parameter.

theorem Cslib.Crypto.GoldreichLevin.polyTime_maskCount {α : Type} {input : α ↪ List Bool} {dimension precision : α → ℕ} (hdimension : Turing.MultiTapeTM.ComputableTidilyInPolyTime dimension input Turing.MultiTapeTM.encUnary) (hprecision : Turing.MultiTapeTM.ComputableTidilyInPolyTime precision input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => maskCount (dimension a) (precision a)) input Turing.MultiTapeTM.encUnary

Computing the logarithmic mask count includes the unary precision arithmetic.

def Cslib.Crypto.GoldreichLevin.nonzeroSelectors (count : ℕ) : List (List Bool)

The selectors for nonempty subsets of the base masks.

theorem Cslib.Crypto.GoldreichLevin.listStrictMajority_nonzeroSelectors (count : ℕ) (vote : List Bool → Bool) : BitString.listStrictMajority (List.map vote (nonzeroSelectors count)) = BitString.strictMajorityOn (nonemptySubsets count) fun (s : Finset (Fin count)) => vote (List.ofFn fun (i : Fin count) => decide (i ∈ s))

The word selectors enumerate exactly the finite decoder's voting subsets, once each.

theorem Cslib.Crypto.GoldreichLevin.enumList_size_polynomial (degree : ℕ) : PolynomiallyBounded fun (n : ℕ) => ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (BitString.enumList (maskCount n (precision degree n)))).length

At fixed precision, the complete encoded guess list has polynomial size.

theorem Cslib.Crypto.GoldreichLevin.polyTime_enumList_maskCount {α : Type} {input : α ↪ List Bool} {parameter : α → ℕ} (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter input Turing.MultiTapeTM.encUnary) (degree : ℕ) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => BitString.enumList (maskCount (parameter a) (precision degree (parameter a)))) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Enumerating at a fixed precision degree includes the cost of computing the mask count.

def Cslib.Crypto.GoldreichLevin.wordCandidate (predictor : List Bool → Bool) (dimension : ℕ) (rows selectors : List (List Bool)) (guess : List Bool) : List Bool

Decode one parity guess by mapping a corrected majority vote over the coordinates.

theorem Cslib.Crypto.GoldreichLevin.polyTime_wordCandidate {α : Type} {input : α ↪ List Bool} {predictor : α → List Bool → Bool} {dimension : α → ℕ} {rows selectors : α → List (List Bool)} {guess : α → List Bool} (hpredictor : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : α × List Bool) => predictor p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hdimension : Turing.MultiTapeTM.ComputableTidilyInPolyTime dimension input Turing.MultiTapeTM.encUnary) (hrows : Turing.MultiTapeTM.ComputableTidilyInPolyTime rows input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hselectors : Turing.MultiTapeTM.ComputableTidilyInPolyTime selectors input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hguess : Turing.MultiTapeTM.ComputableTidilyInPolyTime guess input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => wordCandidate (predictor a) (dimension a) (rows a) (selectors a) (guess a)) input Turing.MultiTapeTM.encBits

Nested maps compose with any predictor certified jointly in its input and query.

theorem Cslib.Crypto.GoldreichLevin.wordCandidate_eq_ofFn {n k : ℕ} (predictor : List Bool → Bool) (masks : Fin k → BitString n) (guess : BitString k) : wordCandidate predictor n (List.ofFn fun (i : Fin k) => List.ofFn (masks i)) (nonzeroSelectors k) (List.ofFn guess) = List.ofFn (candidate (fun (query : BitString n) => predictor (List.ofFn query)) masks guess)

The word program computes exactly the finite decoder's candidate for the same guess.

def Cslib.Crypto.GoldreichLevin.wordCandidates (predictor : List Bool → Bool) (dimension : ℕ) (rows guesses : List (List Bool)) : List (List Bool)

Generate a candidate for every guess, reusing the nonzero selectors across candidates.

theorem Cslib.Crypto.GoldreichLevin.polyTime_wordCandidates {α : Type} {input : α ↪ List Bool} {predictor : α → List Bool → Bool} {dimension : α → ℕ} {rows guesses : α → List (List Bool)} (hpredictor : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : α × List Bool) => predictor p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hdimension : Turing.MultiTapeTM.ComputableTidilyInPolyTime dimension input Turing.MultiTapeTM.encUnary) (hrows : Turing.MultiTapeTM.ComputableTidilyInPolyTime rows input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) (hguesses : Turing.MultiTapeTM.ComputableTidilyInPolyTime guesses input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => wordCandidates (predictor a) (dimension a) (rows a) (guesses a)) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

The guess-list certificate accounts for the number and size of candidate words.

theorem Cslib.Crypto.GoldreichLevin.wordCandidates_eq_map {n k : ℕ} (predictor : List Bool → Bool) (masks : Fin k → BitString n) : wordCandidates predictor n (List.ofFn fun (i : Fin k) => List.ofFn (masks i)) (BitString.enumList k) = List.map List.ofFn (candidateList (fun (query : BitString n) => predictor (List.ofFn query)) masks)

Candidate generation preserves the finite decoder's order and duplicates.

def Cslib.Crypto.GoldreichLevin.wordCheckCandidates (f : List Bool → List Bool) (dimension : ℕ) (image : List Bool) (candidates : List (List Bool)) : List Bool

Return the first matching candidate, defaulting to a zero word of the input dimension.

theorem Cslib.Crypto.GoldreichLevin.polyTime_wordCheckCandidates {α : Type} {input : α ↪ List Bool} {f : List Bool → List Bool} {dimension : α → ℕ} {image : α → List Bool} {candidates : α → List (List Bool)} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hdimension : Turing.MultiTapeTM.ComputableTidilyInPolyTime dimension input Turing.MultiTapeTM.encUnary) (himage : Turing.MultiTapeTM.ComputableTidilyInPolyTime image input Turing.MultiTapeTM.encBits) (hcandidates : Turing.MultiTapeTM.ComputableTidilyInPolyTime candidates input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => wordCheckCandidates f (dimension a) (image a) (candidates a)) input Turing.MultiTapeTM.encBits

Candidate checking composes evaluation, equality, captured search and a runtime fallback.

theorem Cslib.Crypto.GoldreichLevin.wordCheckCandidates_eq_ofFn {n : ℕ} (f : List Bool → List Bool) (image : List Bool) (candidates : List (BitString n)) : wordCheckCandidates f n image (List.map List.ofFn candidates) = List.ofFn (checkCandidates (fun (bits : BitString n) => f (List.ofFn bits)) image candidates)

Searching the word representation preserves the finite decoder's first-match behavior.

def Cslib.Crypto.GoldreichLevin.wordDecode (f : List Bool → List Bool) (predictor : List Bool → Bool) (degree dimension : ℕ) (image masks : List Bool) : List Bool

Decode a predictor using one mask tape, then check the candidates against the image. The predictor may capture arbitrary public data and saved coins independently of that image.

theorem Cslib.Crypto.GoldreichLevin.polyTime_wordDecode {α : Type} {input : α ↪ List Bool} {f : List Bool → List Bool} {predictor : α → List Bool → Bool} {dimension : α → ℕ} {image masks : α → List Bool} (degree : ℕ) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hpredictor : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : α × List Bool) => predictor p.1 p.2) (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hdimension : Turing.MultiTapeTM.ComputableTidilyInPolyTime dimension input Turing.MultiTapeTM.encUnary) (himage : Turing.MultiTapeTM.ComputableTidilyInPolyTime image input Turing.MultiTapeTM.encBits) (hmasks : Turing.MultiTapeTM.ComputableTidilyInPolyTime masks input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => wordDecode f (predictor a) degree (dimension a) (image a) (masks a)) input Turing.MultiTapeTM.encBits

The complete decoder is polynomial-time for each fixed precision degree.

theorem Cslib.Crypto.GoldreichLevin.wordDecode_eq_ofFn (f : List Bool → List Bool) (predictor : List Bool → Bool) (degree dimension : ℕ) (image masks : List Bool) : wordDecode f predictor degree dimension image masks = List.ofFn (checkCandidates (fun (bits : BitString dimension) => f (List.ofFn bits)) image (candidateList (fun (query : BitString dimension) => predictor (List.ofFn query)) (BitString.ofList (maskCount dimension (precision degree dimension) * dimension) masks).block))

The full word decoder agrees with its finite mathematical algorithm for every predictor and mask tape. No assumption about how the predictor obtains its auxiliary data is required.

theorem Cslib.Crypto.GoldreichLevin.uniform_wordDecode (f : List Bool → List Bool) (predictor : List Bool → Bool) (degree dimension : ℕ) (image : List Bool) : PMF.map (wordDecode f predictor degree dimension image) (BitString.uniformList (maskCount dimension (precision degree dimension) * dimension)) = PMF.map List.ofFn (invertFixed (fun (bits : BitString dimension) => f (List.ofFn bits)) (fun (query : BitString dimension) => predictor (List.ofFn query)) (maskCount dimension (precision degree dimension)) image)

Uniform mask bits give exactly the finite inversion experiment for a captured predictor.

theorem Cslib.Crypto.GoldreichLevin.wordDecode_success_ge_half (f : List Bool → List Bool) (predictor : List Bool → Bool) (degree : ℕ) {n : ℕ} (x : BitString n) (h : 1 / 2 + 1 / ↑(precision degree n) / 2 ≤ agreement (fun (query : BitString n) => predictor (List.ofFn query)) x) : 1 / 2 ≤ ((PMF.map (fun (masks : List Bool) => f (wordDecode f predictor degree n (f (List.ofFn x)) masks) == f (List.ofFn x)) (BitString.uniformList (maskCount n (precision degree n) * n))) true).toReal

A sufficiently correlated word predictor yields a valid preimage with probability at least one half. Auxiliary data stay captured in predictor; the recovered preimage need not be x.