Executable extraction of repeated labels #

The program samples a flat Boolean matrix, hashes the labels, and retains every observation and the matrix seed. Its exact law agrees with the finite two-universal family used by the extraction theorems. The supplied input width also defines behavior on malformed sample lists: labels are truncated or padded with false before hashing.

Main definitions #

extractWordLabels, extractWordLabelsIdeal: actual and ideal matrix-extraction programs.

Main results #

isPPTOn_extractWordLabels: certify sampling, normalization, hashing and copying.
SamplablePair.HasGap.extract_indexed_word_labels: computational extraction for one uniformly efficient family of tests and arbitrary valid index choices.
SamplablePair.HasGap.extract_word_labels: the ordinary single-test interface.

References #

Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, Game 2. [Hol06]. The Boolean-matrix implementation replaces the write-up's finite-field hash family.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

source

noncomputable def Cslib.Crypto.Pseudoentropy.extractWordLabels (count outputBits : ℕ) (samples : List (List Bool × Bool)) :

ProbComp (List (List Bool) × List Bool × List Bool)

Extract labels using an explicitly sampled matrix, retaining observations and the full seed.

Instances For

source

noncomputable def Cslib.Crypto.Pseudoentropy.extractWordLabelsIdeal (source : ProbComp (List Bool)) (count outputBits : ℕ) :

ProbComp (List (List Bool) × List Bool × List Bool)

The comparison experiment keeps the observations and independently samples the hash seed and output bits.

Instances For

source

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_extractWordLabels {α : Type} {input : α ↪ List Bool} {count outputBits : α → ℕ} {samples : α → List (List Bool × Bool)} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (houtput : Turing.MultiTapeTM.ComputableTidilyInPolyTime outputBits input Turing.MultiTapeTM.encUnary) (hsamples : Turing.MultiTapeTM.ComputableTidilyInPolyTime samples input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) :

Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) fun (a : α) => extractWordLabels (count a) (outputBits a) (samples a)

Runtime dimensions and sample lists compose into a strict PPT extractor.

source

theorem Cslib.Crypto.Pseudoentropy.eval_extractWordLabels (count outputBits : ℕ) (samples : List (List Bool × Bool)) :

(extractWordLabels count outputBits samples).eval = PMF.map (fun (result : List (List Bool) × BitString (outputBits * count) × BitString outputBits) => (result.1, List.ofFn result.2.1, List.ofFn result.2.2)) (extractLabels (ProbComp.uniform (BitString (outputBits * count))) (fun (seed : BitString (outputBits * count)) (bits : List Bool) => BitString.LinearHash.hash (BitString.blocksEquiv seed) (BitString.ofList count bits)) samples).eval

The finite and word extractors have exactly the same law, even on malformed sample lists.

source

theorem Cslib.Crypto.Pseudoentropy.eval_extractWordLabelsIdeal (source : ProbComp (List Bool)) (count outputBits : ℕ) :

(extractWordLabelsIdeal source count outputBits).eval = PMF.map (fun (result : List (List Bool) × BitString (outputBits * count) × BitString outputBits) => (result.1, List.ofFn result.2.1, List.ofFn result.2.2)) (extractLabelsIdeal source count (ProbComp.uniform (BitString (outputBits * count))))

The ideal word program agrees with the finite ideal distribution and retains the full seed.

source

Probability.IsPPTOn (Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool fun (input : α × List (List Bool × Bool)) => do let result ← extractLabels (ProbComp.uniform (BitString (outputBits input.1 * count input.1))) (fun (seed : BitString (outputBits input.1 * count input.1)) (bits : List Bool) => BitString.LinearHash.hash (BitString.blocksEquiv seed) (BitString.ofList (count input.1) bits)) input.2 test input.1 (result.1, List.ofFn result.2.1, List.ofFn result.2.2)

An ordinary word test after extraction gives the finite test required by the security theorem. Sampling, padding, hashing, and encoding the public data are all charged to PPT. The test and dimensions may depend on any encoded runtime parameter.

source

have count := fun (n : ℕ) => ExtractionSchedule.count n (realization.length n) (inverseSlack n); Negligible fun (n : ℕ) => Game.advantage (do let samples ← OracleComp.replicate (count n) (pair.sample n) let result ← extractWordLabels (count n) (outputBits n (choose n)) samples test n (choose n) result).eval (extractWordLabelsIdeal (Prod.fst <$> pair.sample n) (count n) (outputBits n (choose n)) >>= test n (choose n)).eval

An efficient indexed family of word extractors is computationally uniform along any bounded choice satisfying the entropy budget. The choice is used only in the proof and need not be efficient; the reduction certifies the whole family of tests.

source

have count := fun (n : ℕ) => ExtractionSchedule.count n (realization.length n) (inverseSlack n); Negligible fun (n : ℕ) => Game.advantage (do let samples ← OracleComp.replicate (count n) (pair.sample n) let result ← extractWordLabels (count n) (outputBits n) samples test n result).eval (extractWordLabelsIdeal (Prod.fst <$> pair.sample n) (count n) (outputBits n) >>= test n).eval

Computational label extraction as two ordinary word programs. The client supplies the entropy budget and a certified test; matrix sampling, finite representations, and the uniform prediction reduction are discharged by the library.

Documentation

Complexity.Crypto.Computational.Pseudoentropy.WordExtraction

Executable extraction of repeated labels #

Main definitions #

Main results #

References #