Extracting with a sampled linear hash

The extractor samples a fresh Boolean matrix and returns its complete seed followed by the digest. Its exact law is the finite strong-extraction experiment. Arbitrary randomized tests of the word output satisfy the leftover-hash bound; tests may inspect both seed and digest and need not be efficient. This uses the upstream finite-PMF distance without a competing metric on the infinite type of lists. Uniform strict PPT is certified separately.

Main definitions

• Cslib.BitString.LinearHash.extract: sample and reveal a matrix and its hash output.

Main results

• Cslib.BitString.LinearHash.eval_extract_bind: the complete finite-to-list joint law.
• Cslib.BitString.LinearHash.eval_extract_replicate: extraction from concatenated repeated runs.
• Cslib.BitString.LinearHash.extract_dist_bind_le: leftover hashing for every randomized test with a finite result type, including arbitrary Boolean distinguishers.

References

• T. Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, Section 3.3, Lemma 1.
• I. Haitner, S. Vadhan, The Many Entropies in One-Way Functions, Section 2.4.1, Definition 4 and Lemma 8.

Adapted from Languages/Probabilistic/LinearHash.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing block and finite-distance APIs.

noncomputable def Cslib.BitString.LinearHash.extract (count : ℕ) (input : List Bool) : ProbComp (List Bool)

Sample an independent hash matrix and return its seed followed by the extracted bits.

theorem Cslib.BitString.LinearHash.length_extract (count : ℕ) (input : List Bool) {output : List Bool} (houtput : output ∈ (extract count input).eval.support) : output.length = count * input.length + count

Every extractor output contains the complete matrix seed and exactly count digest bits.

theorem Cslib.BitString.LinearHash.eval_extract_bind {n m : ℕ} (source : PMF (BitString n)) : ((PMF.map List.ofFn source).bind fun (input : List Bool) => (extract m input).eval) = PMF.map (fun (pair : BitString (m * n) × BitString m) => List.ofFn pair.1 ++ List.ofFn pair.2) (Probability.seededHash (Probability.PMF.uniformOfFintype (BitString (m * n))) source fun (seed : BitString (m * n)) => hash (blocksEquiv seed))

The word extractor agrees exactly with the finite strong-extraction experiment.

theorem Cslib.BitString.LinearHash.eval_extract_replicate {width : ℕ} (source : ProbComp (BitString width)) (count outputBits : ℕ) : (do let words ← OracleComp.replicate count (List.ofFn <$> source) extract outputBits words.flatten).eval = PMF.map (fun (result : BitString (outputBits * (count * width)) × BitString outputBits) => List.ofFn result.1 ++ List.ofFn result.2) (Probability.seededHash (Probability.PMF.uniformOfFintype (BitString (outputBits * (count * width)))) (ProbComp.eval (OracleComp.replicate count source)) fun (seed : BitString (outputBits * (count * width))) (values : List (BitString width)) => hash (blocksEquiv seed) (ofList (count * width) (List.map List.ofFn values).flatten))

Hashing concatenated independent fixed-width words has the tuple extraction law.

theorem Cslib.BitString.LinearHash.extract_dist_bind_le {n m : ℕ} (source : PMF (BitString n)) {Result : Type u_1} [Fintype Result] (test : List Bool → PMF Result) : dist (((PMF.map List.ofFn source).bind fun (input : List Bool) => (extract m input).eval).bind test) ((uniformList (m * n + m)).bind test) ≤ √(2 ^ m * Probability.PMF.collisionProbability source) / 2

Every randomized finite-output test of the complete word output satisfies the strong leftover-hash bound. The test has no computational restriction and sees the public seed.