Uniform bounds for indexed predictors

An efficient sampler supplies fresh labeled examples for empirical predictor selection. A single uniform predictor then performs almost as well as every candidate in a polynomial-size family. Consequently a pseudoentropy gap bounds all candidates simultaneously, with any prescribed inverse-polynomial slack. The bound allows the best candidate to vary arbitrarily with the security parameter; that choice is never supplied to the algorithm.

Main definitions

• selectPredictor: validate candidates on fresh examples before predicting the challenge.

Main results

• selectPredictor_error_le: compare with every candidate, charging validation error.
• SamplablePair.HasGap.eventually_indexed_error_ge: one threshold for all candidate indices.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, final proof of Theorem 1. [Hol06]. This empirical selection step prepares the uniform treatment of the entropy guesses in that proof. Its quantitative bound uses the shared concentration and candidate-selection rules.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.Crypto.Pseudoentropy.selectPredictor (count trials : ℕ) (source : ProbComp (List Bool × Bool)) (predict : ℕ → List Bool → ProbComp Bool) (observation : List Bool) : ProbComp Bool

Compare predictors on fresh labeled samples, then use the chosen predictor on the challenge. The challenge's hidden label is never an input to this program.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_selectPredictor {α : Type} {input : α ↪ List Bool} {count trials : α → ℕ} {source : α → ProbComp (List Bool × Bool)} {predict : α → ℕ → List Bool → ProbComp Bool} {observation : α → List Bool} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (htrials : Turing.MultiTapeTM.ComputableTidilyInPolyTime trials input Turing.MultiTapeTM.encUnary) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hpredict : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (x : (α × ℕ) × List Bool) => predict x.1.1 x.1.2 x.2) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observation input Turing.MultiTapeTM.encBits) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => selectPredictor (count a) (trials a) (source a) (predict a) (observation a)

Empirical prediction is strict PPT when the sampler, indexed predictors, and counts are efficient. All callbacks may capture the original input.

theorem Cslib.Crypto.Pseudoentropy.eval_predictionGame_selectPredictor (sample : ℕ → ProbComp (List Bool × Bool)) (predict : ℕ → ℕ → List Bool → ProbComp Bool) (count trials : ℕ → ℕ) (n : ℕ) : (predictionGame sample (fun (n : ℕ) => selectPredictor (count n) (trials n) (sample n) (predict n)) n).eval = (do let i ← OracleComp.selectBest (count n) (trials n) fun (i : ℕ) => predictionGame sample (fun (n : ℕ) => predict n i) n predictionGame sample (fun (n : ℕ) => predict n i) n).eval

Selection is independent of the challenge, so its final correctness game is a fresh trial of the selected candidate.

theorem Cslib.Crypto.Pseudoentropy.selectPredictor_error_le (sample : ℕ → ProbComp (List Bool × Bool)) (predict : ℕ → ℕ → List Bool → ProbComp Bool) (count confidence inverseTolerance : ℕ → ℕ) (n i : ℕ) (hi : i < count n) (htolerance : 0 < inverseTolerance n) : ((predictionGame sample (fun (n : ℕ) => selectPredictor (count n) ((confidence n + 1) * inverseTolerance n ^ 2) (sample n) (predict n)) n).eval false).toReal ≤ ((predictionGame sample (fun (n : ℕ) => predict n i) n).eval false).toReal + 2 / ↑(inverseTolerance n) + ↑(count n) * (1 / 2) ^ confidence n

The selected predictor's error is bounded by every candidate's error plus estimation and selection losses, with the challenge sampled independently of all validation samples.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_indexed_error_ge {pair : SamplablePair} {gap : ℕ → ℝ} (hgap : pair.HasGap gap) (predict : ℕ → ℕ → List Bool → ProbComp Bool) (hpredict : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool fun (x : (ℕ × ℕ) × List Bool) => predict x.1.1 x.1.2 x.2) {count inverseTolerance : ℕ → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (htolerance : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseTolerance Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hpos : ∀ (n : ℕ), 0 < inverseTolerance n) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < count n, (Probability.PMF.conditionalEntropy (pair.joint n) + gap n) / 2 ≤ ((predictionGame pair.sample (fun (n : ℕ) => predict n i) n).eval false).toReal + 1 / ↑(inverseTolerance n)

A pseudoentropy gap bounds every member of a uniformly efficient polynomial-size family at once, allowing any efficient inverse-polynomial slack. No computable choice of index is assumed, and the eventual threshold is common to all indices at each parameter.