The hashed parity inverter as a PPT word program

The reduction samples one saved predictor tape, a hash length, a matrix, a guessed digest, and decoder masks. It then invokes the shared word decoder with the public fields and coins captured by its callback. All sampling uses fair bits, with a fixed polynomial bound for every input.

The coin budget uses the actual framed input encoding: the unary security parameter contributes 2 * n + 1 cells and the parity query another n. All public fields and delimiters are charged. The saved evaluator returns a Boolean directly, without decoding arbitrary output words.

Main definitions

• Cslib.Crypto.Pseudoentropy.HashPair.wordInverter: the functional saved-coin reduction.
• Cslib.Crypto.Pseudoentropy.HashPair.fixedPredictor: one finite deterministic predictor.

Main results

• Cslib.Crypto.Pseudoentropy.HashPair.isPPT_wordInverter: strict uniform PPT.
• Cslib.Crypto.Pseudoentropy.HashPair.wordInverter_eval: the exact finite/list law.
• Cslib.Crypto.Pseudoentropy.HashPair.word_prediction_entropy_le: the complete reduction bound.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 4, Lemma 4. HashReduction supplies the finite bound for our public matrix family and enlarged dyadic range. This module implements its inverter using the word and saved-coin interfaces.

Adapted from Crypto/Computational/Pseudoentropy/WordReduction.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using typed saved seeds and the tidy TM calculus.

def Cslib.Crypto.Pseudoentropy.HashPair.coinBudget (c d n imageLength : ℕ) : ℕ

One polynomial tape budget covers all digest lengths and parity queries for an image.

theorem Cslib.Crypto.Pseudoentropy.HashPair.computableTidilyInPolyTime_coinBudget {α : Type} {encode : α ↪ List Bool} {parameter length : α → ℕ} (c d : ℕ) (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter encode Turing.MultiTapeTM.encUnary) (hlength : Turing.MultiTapeTM.ComputableTidilyInPolyTime length encode Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => coinBudget c d (parameter a) (length a)) encode Turing.MultiTapeTM.encUnary

The shared tape budget is efficient in the parameter and image length.

def Cslib.Crypto.Pseudoentropy.HashPair.predictWithCoins (evaluate : ℕ × List Bool → List Bool → Bool) (n : ℕ) (image : List Bool) (index : ℕ) (matrix digest coins query : List Bool) : Bool

Call the saved-coin predictor on the complete public observation.

theorem Cslib.Crypto.Pseudoentropy.HashPair.computableTidilyInPolyTime_predictWithCoins {α : Type} {encode : α ↪ List Bool} {evaluate : ℕ × List Bool → List Bool → Bool} {parameter index : α → ℕ} {image matrix digest coins query : α → List Bool} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (ℕ × List Bool) × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter encode Turing.MultiTapeTM.encUnary) (himage : Turing.MultiTapeTM.ComputableTidilyInPolyTime image encode Turing.MultiTapeTM.encBits) (hindex : Turing.MultiTapeTM.ComputableTidilyInPolyTime index encode Turing.MultiTapeTM.encUnary) (hmatrix : Turing.MultiTapeTM.ComputableTidilyInPolyTime matrix encode Turing.MultiTapeTM.encBits) (hdigest : Turing.MultiTapeTM.ComputableTidilyInPolyTime digest encode Turing.MultiTapeTM.encBits) (hcoins : Turing.MultiTapeTM.ComputableTidilyInPolyTime coins encode Turing.MultiTapeTM.encBits) (hquery : Turing.MultiTapeTM.ComputableTidilyInPolyTime query encode Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => predictWithCoins evaluate (parameter a) (image a) (index a) (matrix a) (digest a) (coins a) (query a)) encode Turing.MultiTapeTM.encBool

Captured public fields and coins use their ordinary efficiency certificates. The typed callback has a uniformly polynomial bound on every supplied input, not only sampled words.

noncomputable def Cslib.Crypto.Pseudoentropy.HashPair.wordInverter (f : List Bool → List Bool) (evaluate : ℕ × List Bool → List Bool → Bool) (c d degree : ℕ) : Inverter

Guess the unknown hash value and decode, using the same predictor coins for every query.

theorem Cslib.Crypto.Pseudoentropy.HashPair.isPPT_wordInverter {f : List Bool → List Bool} {evaluate : ℕ × List Bool → List Bool → Bool} (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (ℕ × List Bool) × List Bool) => evaluate p.1 p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (c d degree : ℕ) : Probability.IsPPT Turing.MultiTapeTM.encBits (wordInverter f evaluate c d degree)

The complete inverter is one strict PPT program for every parameter and image.

theorem Cslib.Crypto.Pseudoentropy.HashPair.observation_coinBudget_le (c d n : ℕ) (image : List Bool) (index : Fin (hashCount n)) (matrix : BitString (hashCount n * n)) (digest : BitString (↑index + 1)) (query : BitString n) : c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (n, wordObservation image (↑index) (List.ofFn matrix) (List.ofFn digest) (List.ofFn query))).length + 1) ^ d ≤ coinBudget c d n image.length

The tape budget covers every well-formed public observation at this dimension.

def Cslib.Crypto.Pseudoentropy.HashPair.fixedPredictor {Image : Type u_1} (encodeImage : Image → List Bool) (evaluate : ℕ × List Bool → List Bool → Bool) (c d n imageLength : ℕ) (coins : BitString (coinBudget c d n imageLength)) : MatrixPredictor n (hashCount n) Image

A common finite tape turns the word evaluator into a deterministic matrix predictor. The finite image type is represented injectively when relating its inversion experiment.

theorem Cslib.Crypto.Pseudoentropy.HashPair.fixedPredictor_distribution {Image : Type u_1} (encodeImage : Image → List Bool) (adversary : Distinguisher) (evaluate : ℕ × List Bool → List Bool → Bool) (c d : ℕ) (hrealize : ∀ (n : ℕ) (input : List Bool) (budget : ℕ), c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (n, input)).length + 1) ^ d ≤ budget → (adversary n input).eval = PMF.map (evaluate (n, input)) (BitString.uniformList budget)) (n imageLength : ℕ) (image : Image) (hlength : (encodeImage image).length = imageLength) (index : Fin (hashCount n)) (rows : Fin (hashCount n) → BitString n) (digest : BitString (↑index + 1)) (query : BitString n) : PMF.map (fun (coins : BitString (coinBudget c d n imageLength)) => fixedPredictor encodeImage evaluate c d n imageLength coins image index rows digest query) (Probability.PMF.uniformOfFintype (BitString (coinBudget c d n imageLength))) = (adversary n (wordObservation (encodeImage image) (↑index) (List.ofFn (BitString.blocksEquiv.symm rows)) (List.ofFn digest) (List.ofFn query))).eval

Padding the saved tape to the common budget preserves every individual prediction law.

theorem Cslib.Crypto.Pseudoentropy.HashPair.wordInverter_eval {n imageLength : ℕ} {Image : Type u_1} [DecidableEq Image] (f : List Bool → List Bool) (finiteFunction : BitString n → Image) (encodeImage : Image ↪ List Bool) (hf : ∀ (x : Fin n → Bool), f (List.ofFn x) = encodeImage (finiteFunction x)) (evaluate : ℕ × List Bool → List Bool → Bool) (c d degree : ℕ) (image : Image) (hlength : (encodeImage image).length = imageLength) : (wordInverter f evaluate c d degree n (encodeImage image)).eval = PMF.map List.ofFn do let coins ← Probability.PMF.uniformOfFintype (BitString (coinBudget c d n imageLength)) matrixInverter finiteFunction (fixedPredictor (⇑encodeImage) evaluate c d n imageLength coins) (GoldreichLevin.precision degree n) image

The word inverter agrees exactly with the finite inverter after encoding its output. Only the image representation and its fixed width enter this statement.

theorem Cslib.Crypto.Pseudoentropy.HashPair.eval_predictionGame {n imageLength : ℕ} {Image : Type u_1} (f : List Bool → List Bool) (finiteFunction : BitString n → Image) (encodeImage : Image → List Bool) (hf : ∀ (x : Fin n → Bool), f (List.ofFn x) = encodeImage (finiteFunction x)) (hlength : ∀ (image : Image), (encodeImage image).length = imageLength) (adversary : Distinguisher) (evaluate : ℕ × List Bool → List Bool → Bool) (c d : ℕ) (hrealize : ∀ (n : ℕ) (input : List Bool) (budget : ℕ), c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (n, input)).length + 1) ^ d ≤ budget → (adversary n input).eval = PMF.map (evaluate (n, input)) (BitString.uniformList budget)) : (predictionGame (sample f) adversary n).eval = do let coins ← Probability.PMF.uniformOfFintype (BitString (coinBudget c d n imageLength)) matrixPrediction finiteFunction (fixedPredictor encodeImage evaluate c d n imageLength coins)

The complete prediction game agrees with the finite experiment with one independent saved tape. Moving that tape outside the experiment does not change the predictor's distribution.

theorem Cslib.Crypto.Pseudoentropy.HashPair.eval_wordInversionGame {n imageLength : ℕ} {Image : Type u_1} [DecidableEq Image] (f : List Bool → List Bool) (finiteFunction : BitString n → Image) (encodeImage : Image ↪ List Bool) (hf : ∀ (x : Fin n → Bool), f (List.ofFn x) = encodeImage (finiteFunction x)) (hlength : ∀ (image : Image), (encodeImage image).length = imageLength) (evaluate : ℕ × List Bool → List Bool → Bool) (c d degree : ℕ) : (inversionGame f (wordInverter f evaluate c d degree) n).eval = GoldreichLevin.inversionExperiment finiteFunction fun (image : Image) => do let coins ← Probability.PMF.uniformOfFintype (BitString (coinBudget c d n imageLength)) matrixInverter finiteFunction (fixedPredictor (⇑encodeImage) evaluate c d n imageLength coins) (GoldreichLevin.precision degree n) image

The word one-wayness game is the finite inversion experiment under the same image encoding. Success still means finding any preimage.

theorem Cslib.Crypto.Pseudoentropy.HashPair.word_prediction_entropy_le {n imageLength : ℕ} {Image : Type u_1} [Finite Image] (f : List Bool → List Bool) (finiteFunction : BitString n → Image) (encodeImage : Image ↪ List Bool) (hf : ∀ (x : Fin n → Bool), f (List.ofFn x) = encodeImage (finiteFunction x)) (hlength : ∀ (image : Image), (encodeImage image).length = imageLength) (adversary : Distinguisher) (evaluate : ℕ × List Bool → List Bool → Bool) (c d : ℕ) (hrealize : ∀ (n : ℕ) (input : List Bool) (budget : ℕ), c * (((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBits) (n, input)).length + 1) ^ d ≤ budget → (adversary n input).eval = PMF.map (evaluate (n, input)) (BitString.uniformList budget)) (degree : ℕ) (hp : 8 * hashCount n ≤ GoldreichLevin.precision degree n) : 2 * ((predictionGame (sample f) adversary n).eval true).toReal - 1 + Probability.PMF.conditionalEntropy (joint finiteFunction) ≤ 1 - 2 / ↑(hashCount n) + 128 * ↑(Probability.dyadicSize (16 * hashCount n)) ^ 2 * ((inversionGame f (wordInverter f evaluate c d degree) n).eval true).toReal

Holenstein's entropy-versus-prediction bound for the executable word games. Every sampled bit and decoder query is included in the inverter certified by isPPT_wordInverter.