The matrix-hash prediction-to-inversion bound

Split a leaked matrix hash into an almost uniform prefix and a short suffix. The inverter guesses the entire digest uniformly and invokes Goldreich--Levin. Its definition does not use the split point or the size of the image's fiber. Empty prefixes incur no extraction error.

The finite bounds also allow independent saved coins, reused across every decoder query. Pseudoentropy.WordReduction implements the inverter as a word program.

Main definitions

• Cslib.Crypto.Pseudoentropy.matrixPrediction: prediction from a leaked matrix hash.
• Cslib.Crypto.Pseudoentropy.matrixInverter: one inverter for all fibers and hash lengths.

Main results

• Cslib.Crypto.Pseudoentropy.matrixPrediction_entropy_le_of_coins: entropy threshold with independent saved predictor randomness.
• Cslib.Crypto.Pseudoentropy.matrixInverter_success_ge: the resulting polynomial loss.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 4, Lemma 4, Games 1--5. The hash family here is a public Boolean matrix; the suffix-guessing argument is the one developed in Pseudoentropy.Reduction and Probability.Guessing.

Adapted from Crypto/Computational/Pseudoentropy/HashReduction.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, reusing the pinned finite-PMF distance and shared decoder.

@[reducible, inline]

abbrev Cslib.Crypto.Pseudoentropy.MatrixPredictor (n count : ℕ) (Image : Type u_1) : Type u_1

The parity predictor receives the image, length, full public matrix, and leaked digest.

noncomputable def Cslib.Crypto.Pseudoentropy.matrixPrediction {n count : ℕ} [NeZero count] {Image : Type u_1} (f : BitString n → Image) (predictor : MatrixPredictor n count Image) : PMF Bool

The prediction game for the hashed parity construction, with uniform matrices.

noncomputable def Cslib.Crypto.Pseudoentropy.matrixInverter {n count : ℕ} [NeZero count] {Image : Type u_1} [DecidableEq Image] (f : BitString n → Image) (predictor : MatrixPredictor n count Image) (precision : ℕ) (image : Image) : PMF (BitString n)

The inverter guesses a length, matrix, and digest, then invokes the common decoder.

theorem Cslib.Crypto.Pseudoentropy.exists_short_hash_split (size width count : ℕ) (hsize : 0 < size) (hcount : 0 < count) (hwidth : width ≤ Nat.log 2 size + 6) : ∃ (initial : ℕ) (rest : ℕ), width = initial + rest ∧ (if initial = 0 then 0 else 2 * √(2 ^ initial / ↑size)) ≤ 1 / (8 * ↑count) ∧ 2 ^ (rest + 1) ≤ 128 * ↑(Probability.dyadicSize (16 * count)) ^ 2

A digest at most six bits longer than the logarithmic fiber size can be split into an almost uniform prefix and a suffix with polynomially many guesses. This split is used only in the proof; neither the inverter nor the predictor is given the fiber size.

theorem Cslib.Crypto.Pseudoentropy.matrix_fiber_correlation_le {n count initial rest : ℕ} {Image : Type u_1} [DecidableEq Image] (f : BitString n → Image) (image : Image) [Nonempty { x : BitString n // f x = image }] (hlen : initial + rest ≤ count) (predictor : (Fin count → BitString n) → BitString (initial + rest) → BitString n → Bool) (precision : ℕ) (hp : 0 < precision) : ∑ rows : Fin count → BitString n, ((Probability.PMF.uniformOfFintype (Fin count → BitString n)) rows).toReal * ∑ x : { x : BitString n // f x = image }, ((Probability.PMF.uniformOfFintype { x : BitString n // f x = image }) x).toReal * (2 * GoldreichLevin.agreement (predictor rows (BitString.LinearHash.hash (rows ∘ Fin.castLE hlen) ↑x)) ↑x - 1) ≤ (1 / ↑precision + if initial = 0 then 0 else 2 * √(2 ^ initial / ↑(Nat.card { x : BitString n // f x = image }))) + 2 ^ (rest + 1) * ((PMF.map (fun (x : BitString n) => f x == image) (guessInverter f predictor (Probability.PMF.uniformOfFintype (Fin count → BitString n)) precision image)) true).toReal

On each fiber, prediction from a matrix hash is bounded by the decoder's accuracy, the prefix extraction error, and inversion with a uniform digest guess. The public matrix may contain additional unused rows.

theorem Cslib.Crypto.Pseudoentropy.matrix_fiber_correlation_le_of_length {n count width : ℕ} {Image : Type u_1} [DecidableEq Image] (f : BitString n → Image) (image : Image) [Nonempty { x : BitString n // f x = image }] (hcount : 0 < count) (hlen : width ≤ count) (hwidth : width ≤ Nat.log 2 (Nat.card { x : BitString n // f x = image }) + 6) (predictor : (Fin count → BitString n) → BitString width → BitString n → Bool) (precision : ℕ) (hp : 8 * count ≤ precision) : ∑ rows : Fin count → BitString n, ((Probability.PMF.uniformOfFintype (Fin count → BitString n)) rows).toReal * ∑ x : { x : BitString n // f x = image }, ((Probability.PMF.uniformOfFintype { x : BitString n // f x = image }) x).toReal * (2 * GoldreichLevin.agreement (predictor rows (BitString.LinearHash.hash (rows ∘ Fin.castLE hlen) ↑x)) ↑x - 1) ≤ 1 / (4 * ↑count) + 128 * ↑(Probability.dyadicSize (16 * count)) ^ 2 * ((PMF.map (fun (x : BitString n) => f x == image) (guessInverter f predictor (Probability.PMF.uniformOfFintype (Fin count → BitString n)) precision image)) true).toReal

A hash within six bits of the logarithmic fiber size has a uniform polynomial reduction loss. This one inverter works for every fiber; their sizes determine only its analysis.

theorem Cslib.Crypto.Pseudoentropy.matrix_fiber_mean_correlation_le {n count : ℕ} [NeZero count] {Image : Type u_1} [DecidableEq Image] (f : BitString n → Image) (image : Image) [Nonempty { x : BitString n // f x = image }] (hcount : n + 6 ≤ count) (predictor : MatrixPredictor n count Image) (precision : ℕ) (hp : 8 * count ≤ precision) : ∑ i : Fin count, ((Probability.PMF.uniformOfFintype (Fin count)) i).toReal * ∑ rows : Fin count → BitString n, ((Probability.PMF.uniformOfFintype (Fin count → BitString n)) rows).toReal * ∑ x : { x : BitString n // f x = image }, ((Probability.PMF.uniformOfFintype { x : BitString n // f x = image }) x).toReal * (2 * GoldreichLevin.agreement (predictor image i rows (BitString.LinearHash.hash (rows ∘ Fin.castLE ⋯) ↑x)) ↑x - 1) ≤ 1 - (↑(Nat.log 2 (Nat.card { x : BitString n // f x = image })) + 6) / ↑count + 1 / (4 * ↑count) + 128 * ↑(Probability.dyadicSize (16 * count)) ^ 2 * ((PMF.map (fun (x : BitString n) => f x == image) (matrixInverter f predictor precision image)) true).toReal

Averaging all hash lengths removes the restriction on digest size. A range at least n + 6 makes the truncation threshold valid even for the largest possible fiber.

theorem Cslib.Crypto.Pseudoentropy.matrixPrediction_correlation_le {n count : ℕ} [NeZero count] {Image : Type u_1} [Finite Image] [DecidableEq Image] (f : BitString n → Image) (hcount : n + 6 ≤ count) (predictor : MatrixPredictor n count Image) (precision : ℕ) (hp : 8 * count ≤ precision) : 2 * ((matrixPrediction f predictor) true).toReal - 1 ≤ 1 - (∑ x : BitString n, ((Probability.PMF.uniformOfFintype (BitString n)) x).toReal * Real.logb 2 ↑(Nat.card { y : BitString n // f y = f x }) + 4) / ↑count + 128 * ↑(Probability.dyadicSize (16 * count)) ^ 2 * ((GoldreichLevin.inversionExperiment f (matrixInverter f predictor precision)) true).toReal

The complete finite reduction bound, averaged over images as well as hash lengths. All fibers share one inverter and one precision; no regularity or injectivity is required.

theorem Cslib.Crypto.Pseudoentropy.matrixPrediction_entropy_le {n count : ℕ} [NeZero count] {Image : Type u_1} [Finite Image] [DecidableEq Image] (f : BitString n → Image) (hcount : n + 6 ≤ count) (predictor : MatrixPredictor n count Image) (precision : ℕ) (hp : 8 * count ≤ precision) : 2 * ((matrixPrediction f predictor) true).toReal - 1 + Probability.PMF.conditionalEntropy (HashPair.joint f) ≤ 1 - 2 / ↑count + 128 * ↑(Probability.dyadicSize (16 * count)) ^ 2 * ((GoldreichLevin.inversionExperiment f (matrixInverter f predictor precision)) true).toReal

Prediction beyond the hashed pair's entropy threshold forces inversion with polynomial loss. This is the finite content of Holenstein's Lemma 4, for public matrix hashing.

theorem Cslib.Crypto.Pseudoentropy.matrixPrediction_entropy_le_of_coins {n count : ℕ} [NeZero count] {Image : Type u_1} {Coins : Type u_2} [Finite Image] [DecidableEq Image] [Finite Coins] (f : BitString n → Image) (hcount : n + 6 ≤ count) (coins : PMF Coins) (predictor : Coins → MatrixPredictor n count Image) (precision : ℕ) (hp : 8 * count ≤ precision) : 2 * ((coins.bind fun (seed : Coins) => matrixPrediction f (predictor seed)) true).toReal - 1 + Probability.PMF.conditionalEntropy (HashPair.joint f) ≤ 1 - 2 / ↑count + 128 * ↑(Probability.dyadicSize (16 * count)) ^ 2 * ((GoldreichLevin.inversionExperiment f fun (image : Image) => coins.bind fun (seed : Coins) => matrixInverter f (predictor seed) precision image) true).toReal

The entropy reduction survives independent predictor randomness. The inverter samples one coin tape and reuses the resulting deterministic predictor throughout all decoder calls.

theorem Cslib.Crypto.Pseudoentropy.matrixInverter_success_ge {n count : ℕ} [NeZero count] {Image : Type u_1} [Finite Image] [DecidableEq Image] (f : BitString n → Image) (hcount : n + 6 ≤ count) (predictor : MatrixPredictor n count Image) (precision : ℕ) (hp : 8 * count ≤ precision) (hprediction : 1 - Probability.PMF.conditionalEntropy (HashPair.joint f) - 1 / ↑count ≤ 2 * ((matrixPrediction f predictor) true).toReal - 1) : 1 / (128 * ↑count * ↑(Probability.dyadicSize (16 * count)) ^ 2) ≤ ((GoldreichLevin.inversionExperiment f (matrixInverter f predictor precision)) true).toReal

Beating the entropy threshold by 1 / count yields inverse-polynomial inversion success. Since dyadicSize (16 * count) ≤ 32 * count + 2, the denominator is cubic in the hash range.