The hashed parity pair

Reveal a function image, a random hash length, a public matrix, the corresponding hash prefix, and an independent parity query. The hidden bit is the input's inner product with the query.

joint gives the finite joint distribution and sample is its word implementation. The entropy bound and the strict PPT certificate are proved here. pair packages the sampler and its exact finite law. HashReduction proves the finite prediction-to-inversion bound, WordReduction implements that reduction, and OneWay derives the computational prediction gap.

Main definitions

• Cslib.Crypto.Pseudoentropy.HashPair.joint: the complete finite hashed-parity experiment.
• Cslib.Crypto.Pseudoentropy.HashPair.sample: its executable sampler.
• Cslib.Crypto.Pseudoentropy.HashPair.pair: package the exact law and efficiency certificate.

Main results

• Cslib.Crypto.Pseudoentropy.HashPair.conditionalEntropy_joint_le: the entropy upper bound.
• Cslib.Crypto.Pseudoentropy.HashPair.isPPTOn_sample: uniform strict PPT sampling.
• Cslib.Crypto.Pseudoentropy.HashPair.eval_sample: exact agreement of the two representations.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 4, equations (4) and (5), and Lemma 3. We use Boolean matrices in place of field multiplication. The executable sampler chooses the hash length exactly uniformly in a dyadic range, avoiding the sampling approximation in footnote 3. The entropy bound holds for any positive number of possible hash lengths.

Adapted from Crypto/Computational/Pseudoentropy/HashPair.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared bit-string and tidy machine APIs.

def Cslib.Crypto.Pseudoentropy.HashPair.hashCount (n : ℕ) : ℕ

The number of possible hash lengths. Six extra lengths leave room for the truncation threshold in the inversion proof; rounding up makes sampling exact with fair bits.

instance Cslib.Crypto.Pseudoentropy.HashPair.instNeZeroNatHashCount (n : ℕ) : NeZero (hashCount n)

theorem Cslib.Crypto.Pseudoentropy.HashPair.hashCount_ge (n : ℕ) : n + 6 ≤ hashCount n

Every fiber's logarithmic size plus six lies inside the sampled hash range.

theorem Cslib.Crypto.Pseudoentropy.HashPair.hashCount_le (n : ℕ) : hashCount n ≤ 2 * (n + 7)

The enlarged hash range is still linear in the input length.

theorem Cslib.Crypto.Pseudoentropy.HashPair.hashCount_polynomiallyBounded : PolynomiallyBounded hashCount

Sampling among the enlarged hash lengths requires only a polynomial range.

theorem Cslib.Crypto.Pseudoentropy.HashPair.computableTidilyInPolyTime_hashCount {α : Type} {encode : α ↪ List Bool} {parameter : α → ℕ} (hparameter : Turing.MultiTapeTM.ComputableTidilyInPolyTime parameter encode Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => hashCount (parameter a)) encode Turing.MultiTapeTM.encUnary

Compute the sampling range from an efficiently available unary parameter.

@[reducible, inline]

abbrev Cslib.Crypto.Pseudoentropy.HashPair.Seed (n count : ℕ) : Type

A flat matrix seed and an independent parity query, both retained in the public output.

@[reducible, inline]

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

A public observation records the hash length and exactly that many hash bits.

def Cslib.Crypto.Pseudoentropy.HashPair.prefixHash {n count : ℕ} (i : Fin count) (seed : Seed n count) (x : BitString n) : BitString (↑i + 1)

Hash with the requested initial rows of the public matrix.

theorem Cslib.Crypto.Pseudoentropy.HashPair.prefixHash_isTwoUniversal {n count : ℕ} (i : Fin count) : Probability.IsTwoUniversal (Probability.PMF.uniformOfFintype (Seed n count)) (prefixHash i)

The query can be included in the public seed without changing hash universality.

noncomputable def Cslib.Crypto.Pseudoentropy.HashPair.joint {n count : ℕ} [NeZero count] {Image : Type u_1} (f : BitString n → Image) : PMF (Observation n count Image × Bool)

The public observation and hidden parity bit under independent uniform inputs.

theorem Cslib.Crypto.Pseudoentropy.HashPair.conditionalEntropy_joint_le {n count : ℕ} [NeZero count] {Image : Type u_1} [Finite Image] (f : BitString n → Image) : Probability.PMF.conditionalEntropy (joint f) ≤ ((∑ x : BitString n, Real.logb 2 ↑(Nat.card { y : BitString n // f y = f x })) / 2 ^ n + 2) / ↑count

Holenstein's entropy bound for the complete hashed parity experiment. No regularity, injectivity, or computational hardness of the function is assumed.

def Cslib.Crypto.Pseudoentropy.HashPair.wordObservation (image : List Bool) (index : ℕ) (matrix digest query : List Bool) : List Bool

Self-delimiting encoding of the five public fields.

theorem Cslib.Crypto.Pseudoentropy.HashPair.computableTidilyInPolyTime_wordObservation {α : Type} {encode : α ↪ List Bool} {image matrix digest query : α → List Bool} {index : α → ℕ} (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) (hquery : Turing.MultiTapeTM.ComputableTidilyInPolyTime query encode Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => wordObservation (image a) (index a) (matrix a) (digest a) (query a)) encode Turing.MultiTapeTM.encBits

Assemble the public fields using the ordinary tuple encoding.

def Cslib.Crypto.Pseudoentropy.HashPair.encodeObservation {n count : ℕ} {Image : Type u_1} (encodeImage : Image → List Bool) (observation : Observation n count Image) : List Bool

Encode a finite public observation using the chosen image representation.

theorem Cslib.Crypto.Pseudoentropy.HashPair.encodeObservation_injective {n count : ℕ} {Image : Type u_1} (encodeImage : Image ↪ List Bool) : Function.Injective (encodeObservation ⇑encodeImage)

Encoding loses none of the public information, even though the digest's width varies.

noncomputable def Cslib.Crypto.Pseudoentropy.HashPair.sample (f : List Bool → List Bool) (n : ℕ) : ProbComp (List Bool × Bool)

Sample the hashed parity pair using only fair bits and ordinary word operations.

theorem Cslib.Crypto.Pseudoentropy.HashPair.isPPTOn_sample (f : List Bool → List Bool) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) : Probability.IsPPTOn Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) (sample f)

The construction is strict PPT whenever the given function is polynomial time.

theorem Cslib.Crypto.Pseudoentropy.HashPair.eval_sample {n : ℕ} {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)) : (sample f n).eval = PMF.map (fun (pair : Observation n (hashCount n) Image × Bool) => (encodeObservation encodeImage pair.1, pair.2)) (joint finiteFunction)

The executable observation and hidden bit have exactly the finite joint distribution.

noncomputable def Cslib.Crypto.Pseudoentropy.HashPair.pair {Image : ℕ → Type} [∀ (n : ℕ), Finite (Image n)] (f : List Bool → List Bool) (hf : Turing.MultiTapeTM.ComputableTidilyInPolyTime f Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (finiteFunction : (n : ℕ) → BitString n → Image n) (encodeImage : (n : ℕ) → Image n ↪ List Bool) (hencode : ∀ (n : ℕ) (x : Fin n → Bool), f (List.ofFn x) = (encodeImage n) (finiteFunction n x)) : SamplablePair

Package the efficient sampler with its finite observation type and exact joint law. The image representation is needed for entropy bookkeeping, not as an extra algorithmic oracle.