Guessing the remainder of a partially uniform string

If the prefix of a public string is close to uniform, replacing the whole string by a uniform guess costs the size of the suffix space, together with the prefix's statistical error. The score may be any number in [0, 1], including a decoder's probability of returning a valid preimage.

Main results

• Cslib.Probability.score_le_uniform_guess: replacing a partially uniform string by a guess.
• Cslib.Probability.IsTwoUniversal.score_le_uniform_guess: a universal hash supplies the error.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 4, Lemma 4, Games 2--5. We apply the guessing argument directly to a nonnegative success score, so no separate maximization of signed prediction advantage over preimages is needed.

Adapted from Probability/Guessing.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the pinned finite-PMF distance.

theorem Cslib.Probability.score_le_uniform_guess {Seed : Type u_1} {Prefix : Type u_2} {Suffix : Type u_3} [Fintype Seed] [Fintype Prefix] [Fintype Suffix] [Nonempty Prefix] [Nonempty Suffix] (real : PMF (Seed × Prefix × Suffix)) (seed : PMF Seed) (score : Seed → Prefix × Suffix → ℝ) (hscore : ∀ (s : Seed) (z : Prefix × Suffix), 0 ≤ score s z ∧ score s z ≤ 1) : ∑ pair : Seed × Prefix × Suffix, (real pair).toReal * score pair.1 pair.2 ≤ 2 * dist (PMF.map (fun (pair : Seed × Prefix × Suffix) => (pair.1, pair.2.1)) real) (seed.bind fun (s : Seed) => PMF.map (fun (x : Prefix) => (s, x)) (PMF.uniformOfFintype Prefix)) + ↑(Fintype.card Suffix) * ∑ s : Seed, (seed s).toReal * ∑ z : Prefix × Suffix, ((PMF.uniformOfFintype (Prefix × Suffix)) z).toReal * score s z

A uniform suffix guess loses at most its cardinality. The prefix need only be statistically close to uniform given the public seed; the full original string may depend on that seed.

theorem Cslib.Probability.IsTwoUniversal.score_le_uniform_guess {Seed : Type u_1} {Prefix : Type u_2} {Suffix : Type u_3} [Fintype Seed] [Fintype Prefix] [Fintype Suffix] [Nonempty Prefix] [Nonempty Suffix] {Input : Type u_4} [Fintype Input] {seed : PMF Seed} {hash : Seed → Input → Prefix × Suffix} (hhash : IsTwoUniversal seed fun (s : Seed) (x : Input) => (hash s x).1) (source : PMF Input) (score : Seed → Prefix × Suffix → ℝ) (hscore : ∀ (s : Seed) (z : Prefix × Suffix), 0 ≤ score s z ∧ score s z ≤ 1) : ∑ s : Seed, (seed s).toReal * ∑ x : Input, (source x).toReal * score s (hash s x) ≤ √(↑(Fintype.card Prefix) * PMF.collisionProbability source) + ↑(Fintype.card Suffix) * ∑ s : Seed, (seed s).toReal * ∑ z : Prefix × Suffix, ((PMF.uniformOfFintype (Prefix × Suffix)) z).toReal * score s z

If a hash prefix is two-universal, the leftover hash lemma bounds the cost of replacing the complete digest by a uniform guess. The suffix itself need not be a universal hash.