Output collisions of one-way functions

Independently guessing an n-bit preimage inverts f exactly when two independent images collide. The guesser is a uniform strict PPT program, so any OWF has negligible output collision probability. No injectivity, regularity or length-preservation assumption is used. This necessary entropy condition alone does not supply the surplus needed by a PRG.

Main results

• Cslib.Crypto.output_collision_eq_inversion: the independent-guess experiment.
• Cslib.Crypto.OneWay.output_collision_negligible: negligible output collisions.

References

The general OWF-to-PRG development follows T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Sections 4–5. This elementary guessing argument is separate from its stronger pseudoentropy-pair construction.

Adapted from Crypto/Computational/OneWay/Collision.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared nonnegative game API.

theorem Cslib.Crypto.output_collision_eq_inversion (f : List Bool → List Bool) (n : ℕ) : Probability.PMF.collisionProbability (PMF.map f (BitString.uniformList n)) = ↑(Game.succProbability (inversionGame f (fun (n : ℕ) (x : List Bool) => BitString.sampleList n) n).eval)

A fresh independent preimage guess succeeds exactly with the output collision probability.

theorem Cslib.Crypto.OneWay.output_collision_negligible {f : List Bool → List Bool} (hf : OneWay f) : Negligible fun (n : ℕ) => (Probability.PMF.collisionProbability (PMF.map f (BitString.uniformList n))).toNNReal

One-wayness forces negligible output collisions, even for variable-length images. Real.toNNReal is exact here because collision probability is nonnegative.