Statistical extraction from a sampler's seed

The first component hashes public observations; the third hashes the original sampler seeds while revealing every observation and label. Its conditional entropy is exactly the seed length minus the two visible entropy terms. Both use the same repetition schedule as label extraction. The program retains unused coins and never samples a conditional distribution. Zero output bits remain valid even when a component has no entropy left.

Main results

• observation_extraction, observation_word_extraction: extract public-observation entropy.
• remainingSeed_extraction, remainingSeed_word_extraction: extract the remaining sampler entropy while retaining every observation, hidden label, and public hash seed.

All statements admit every randomized test of the joint output, without a computational restriction on the test or an efficient entropy estimate.

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]. We use the shared seed-information concentration schedule.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.observation_extraction {pair : SamplablePair} (saved : pair.SeedRealization) (inverseSlack outputBits : ℕ → ℕ) {Key : ℕ → Type} [(n : ℕ) → Fintype (Key n)] (key : (n : ℕ) → ProbComp (Key n)) (hash : (n : ℕ) → Key n → List (pair.Observation n) → BitString (outputBits n)) (hhash : ∀ (n : ℕ), Probability.IsTwoUniversal (key n).eval fun (key : Key n) (values : Fin (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) → pair.Observation n) => hash n key (List.ofFn values)) (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))) : Game.Indistinguishable (fun (test : (n : ℕ) → Key n × BitString (outputBits n) → Game) (n : ℕ) => (Probability.seededHash (key n).eval (ProbComp.eval (OracleComp.replicate (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) (Prod.fst <$> pair.latentSample n))) (hash n)).bind (test n)) (fun (test : (n : ℕ) → Key n × BitString (outputBits n) → Game) (n : ℕ) => do let k ← (key n).eval let result ← PMF.map (fun (x : BitString (outputBits n)) => (k, x)) (Probability.PMF.uniformOfFintype (BitString (outputBits n))) test n result) fun (x : (n : ℕ) → Key n × BitString (outputBits n) → Game) => True

Repeated public observations supply their Shannon entropy to the first extractor.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.observation_word_extraction {pair : SamplablePair} (saved : pair.SeedRealization) (inverseSlack outputBits : ℕ → ℕ) {Key : ℕ → Type} [(n : ℕ) → Fintype (Key n)] (key : (n : ℕ) → ProbComp (Key n)) (hash : (n : ℕ) → Key n → List (List Bool) → BitString (outputBits n)) (hhash : ∀ (n : ℕ), Probability.IsTwoUniversal (key n).eval fun (key : Key n) (values : Fin (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) → pair.Observation n) => hash n key (List.map (⇑(pair.encode n)) (List.ofFn values))) (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))) : Game.Indistinguishable (fun (test : (n : ℕ) → Key n × BitString (outputBits n) → Game) (n : ℕ) => (Probability.seededHash (key n).eval (ProbComp.eval (OracleComp.replicate (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) (Prod.fst <$> pair.sample n))) (hash n)).bind (test n)) (fun (test : (n : ℕ) → Key n × BitString (outputBits n) → Game) (n : ℕ) => do let k ← (key n).eval let result ← PMF.map (fun (x : BitString (outputBits n)) => (k, x)) (Probability.PMF.uniformOfFintype (BitString (outputBits n))) test n result) fun (x : (n : ℕ) → Key n × BitString (outputBits n) → Game) => True

The first statistical transition on ordinary sampled observation words. Its hash's finite two-universality premise includes the public encoding; no observation is sampled conditionally.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.remainingSeed_extraction {pair : SamplablePair} (saved : pair.SeedRealization) (inverseSlack outputBits : ℕ → ℕ) {Key : ℕ → Type} [(n : ℕ) → Fintype (Key n)] (key : (n : ℕ) → ProbComp (Key n)) (hash : (n : ℕ) → Key n → List (BitString (saved.length n)) → BitString (outputBits n)) (hhash : ∀ (n : ℕ), Probability.IsTwoUniversal (key n).eval fun (key : Key n) (values : Fin (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) → BitString (saved.length n)) => hash n key (List.ofFn values)) (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))) : Game.Indistinguishable (fun (test : (n : ℕ) → List (pair.Observation n × Bool) × Key n × BitString (outputBits n) → Game) (n : ℕ) => (OracleComp.replicate (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) (saved.latentSampleWithSeed n) >>= extractLabels (key n) (hash n)).eval.bind (test n)) (fun (test : (n : ℕ) → List (pair.Observation n × Bool) × Key n × BitString (outputBits n) → Game) (n : ℕ) => (extractLabelsIdeal (pair.latentSample n) (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) (key n)).bind (test n)) fun (x : (n : ℕ) → List (pair.Observation n × Bool) × Key n × BitString (outputBits n) → Game) => True

Extract the unused seed entropy, preserving the complete pair output and hash seed. The entropy chain rule pays for both the public observations and the labels already revealed.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.SeedRealization.remainingSeed_word_extraction {pair : SamplablePair} (saved : pair.SeedRealization) (inverseSlack outputBits : ℕ → ℕ) {Key : ℕ → Type} [(n : ℕ) → Fintype (Key n)] (key : (n : ℕ) → ProbComp (Key n)) (hash : (n : ℕ) → Key n → List (List Bool) → BitString (outputBits n)) (hhash : ∀ (n : ℕ), Probability.IsTwoUniversal (key n).eval fun (key : Key n) (values : Fin (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) → BitString (saved.length n)) => hash n key (List.map List.ofFn (List.ofFn values))) (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))) : Game.Indistinguishable (fun (test : (n : ℕ) → List (List Bool × Bool) × Key n × BitString (outputBits n) → Game) (n : ℕ) => (OracleComp.replicate (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) (saved.sampleWithSeed n) >>= extractLabels (key n) (hash n)).eval.bind (test n)) (fun (test : (n : ℕ) → List (List Bool × Bool) × Key n × BitString (outputBits n) → Game) (n : ℕ) => (extractLabelsIdeal (pair.sample n) (ExtractionSchedule.count n (saved.length n) (inverseSlack n)) (key n)).bind (test n)) fun (x : (n : ℕ) → List (List Bool × Bool) × Key n × BitString (outputBits n) → Game) => True

The remaining-seed transition for the actual word sampler. Every observation and label stays public; finite representations are confined to the two-universality hypothesis.