Executable extraction of observations and retained seeds

The first and third components use the same matrix extractor as label extraction. Concatenating fixed-width sampler seeds supplies an injective input representation. Public observations first receive self-delimiting padding, since their lengths can vary. Each program retains its complete independent matrix seed. Statistical transitions quantify over every randomized Boolean test of the complete output, with no efficiency restriction on the test.

Main definitions

• extractWordObservations: pad and hash observations, returning the matrix seed and digest.
• extractWordSeeds: hash retained sampler seeds while preserving all observations and labels.

Main results

• isPPTOn_extractWordObservations, isPPTOn_extractWordSeeds: strict PPT certificates.
• SeedRealization.extract_word_observations, SeedRealization.extract_word_seeds: the statistical transitions for the actual word programs, including their full public seeds.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5, the first and third extractors and Games 0--1. [Hol06].

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

noncomputable def Cslib.Crypto.Pseudoentropy.extractWordObservations (bound outputBits : ℕ) (observations : List (List Bool)) : ProbComp (List Bool)

Pad observations injectively, concatenate their blocks, and return a fresh hash seed and digest as one word. The seed is part of the output, as in the strong extractor.

theorem Cslib.Crypto.Pseudoentropy.length_extractWordObservations (bound outputBits : ℕ) (observations : List (List Bool)) (hbound : ∀ observation ∈ observations, observation.length ≤ bound) {output : List Bool} (houtput : output ∈ (extractWordObservations bound outputBits observations).eval.support) : output.length = outputBits * (observations.length * (2 * bound + 1)) + outputBits

Bounded observations give a fixed output length, including the complete public seed.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_extractWordObservations {α : Type} {input : α ↪ List Bool} {bound outputBits : α → ℕ} {observations : α → List (List Bool)} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (houtput : Turing.MultiTapeTM.ComputableTidilyInPolyTime outputBits input Turing.MultiTapeTM.encUnary) (hobservations : Turing.MultiTapeTM.ComputableTidilyInPolyTime observations input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Probability.IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => extractWordObservations (bound a) (outputBits a) (observations a)

Observation padding and concatenation compose with the matrix extractor.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.extract_word_observations {pair : SamplablePair} (saved : pair.SeedRealization) (bound inverseSlack outputBits : ℕ → ℕ) (hbound : ∀ (n : ℕ), ∀ observation ∈ (PMF.map Prod.fst (pair.joint n)).support, ((pair.encode n) observation).length ≤ bound n) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, outputBits n = 0 ∨ ↑(outputBits n) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n))) : have count := fun (n : ℕ) => ExtractionSchedule.count n (saved.length n) (inverseSlack n); Game.Indistinguishable (fun (test : ℕ → List Bool → Game) (n : ℕ) => (OracleComp.replicate (count n) (Prod.fst <$> pair.sample n) >>= extractWordObservations (bound n) (outputBits n)).eval.bind (test n)) (fun (test : ℕ → List Bool → Game) (n : ℕ) => (BitString.uniformList (outputBits n * (count n * (2 * bound n + 1)) + outputBits n)).bind (test n)) fun (x : ℕ → List Bool → Game) => True

The first statistical transition with an executable hash and self-delimiting padding. Only supported observations need to fit the bound; exists_observationBound supplies an efficient bound for every PPT sampler. The uniform comparison includes the entire matrix seed.

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

Hash complete sampler seeds while retaining every sampled observation and label.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_extractWordSeeds {α : Type} {input : α ↪ List Bool} {count seedBits outputBits : α → ℕ} {samples : α → List ((List Bool × Bool) × List Bool)} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hseed : Turing.MultiTapeTM.ComputableTidilyInPolyTime seedBits 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.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) Turing.MultiTapeTM.encBits))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)) fun (a : α) => extractWordSeeds (count a) (seedBits a) (outputBits a) (samples a)

Seed-block concatenation composes with the shared matrix extractor's PPT certificate.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.extract_word_seeds {pair : SamplablePair} (saved : pair.SeedRealization) (inverseSlack outputBits : ℕ → ℕ) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, outputBits n = 0 ∨ ↑(outputBits n) + 2 * ↑(ExtractionSchedule.slack n (saved.length n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (saved.length n) (inverseSlack n)) * (↑(saved.length n) - Probability.PMF.entropy (PMF.map Prod.fst (pair.joint n)) - Probability.PMF.conditionalEntropy (pair.joint n))) : have count := fun (n : ℕ) => ExtractionSchedule.count n (saved.length n) (inverseSlack n); Game.Indistinguishable (fun (test : ℕ → List (List Bool × Bool) × List Bool × List Bool → Game) (n : ℕ) => (OracleComp.replicate (count n) (saved.sampleWithSeed n) >>= extractWordSeeds (count n) (saved.length n) (outputBits n)).eval.bind (test n)) (fun (test : ℕ → List (List Bool × Bool) × List Bool × List Bool → Game) (n : ℕ) => (extractMatrixLabelsIdeal (pair.sample n) (count n) (count n * saved.length n) (outputBits n)).eval.bind (test n)) fun (x : ℕ → List (List Bool × Bool) × List Bool × List Bool → Game) => True

The third statistical transition for ordinary programs, with matrix universality discharged. The ideal program preserves the complete pair output and independently samples seed and bits.