Repeated extraction with public side information

Sample a list of observation-label pairs, hash its labels, and retain the observations and the complete independent hash seed. Labels may be arbitrary finite values, including observations or saved sampler seeds. Boolean labels retain their ordinary word-based PPT interface.

The exact product law and conditional-entropy extraction bound are shared by all three parts of the pseudoentropy construction. The ideal experiment preserves the original public marginal.

The statistical statements quantify over every randomized finite-output test of the complete output, including every Boolean test, with no computational restriction. This uses the existing finite-PMF metric without requiring a metric on the infinite ambient type of lists.

Main definitions

• extractLabels, extractLabelsIdeal: real extraction and the ideal public-marginal experiment.

Main results

• eval_replicate_extractLabels: exact agreement with the finite product experiment.
• eval_replicate_extractLabels_map_pair: transport the complete experiment from a sampling law.
• extractLabels_dist_bind_le: conditional entropy bounds every randomized finite-output test.
• extractLabels_indistinguishable: statistical security for the common repetition schedule.
• isPPTOn_extractLabels, isPPTOn_extractLabels_list: strict PPT with raw or framed labels.

References

• Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 3.3 and Section 5, Games 0--2. [Hol06]. The statistical bound uses the seed-information concentration variant documented in Complexity.Probability.EntropyExtraction.

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the shared nonnegative game API.

def Cslib.Crypto.Pseudoentropy.extractLabels {Observation Label Seed Output : Type} (seed : ProbComp Seed) (hash : Seed → List Label → Output) (samples : List (Observation × Label)) : ProbComp (List Observation × Seed × Output)

Hash the sampled labels, retaining every public observation and the independent hash seed.

noncomputable def Cslib.Crypto.Pseudoentropy.extractLabelsIdeal {Observation Seed Output : Type} [Fintype Output] [Nonempty Output] (source : ProbComp Observation) (count : ℕ) (seed : ProbComp Seed) : PMF (List Observation × Seed × Output)

Preserve the sampled observations and public seed, replacing the extracted labels by an independent uniform output. The ambient observation and seed types need not be finite.

theorem Cslib.Crypto.Pseudoentropy.extractLabelsIdeal_map_observation {α β Seed Output : Type} [Fintype Output] [Nonempty Output] (observe : α → β) (source : ProbComp α) (count : ℕ) (seed : ProbComp Seed) {encoded : ProbComp β} (hsource : encoded.eval = PMF.map observe source.eval) : PMF.map (fun (result : List α × Seed × Output) => (List.map observe result.1, result.2)) (extractLabelsIdeal source count seed) = extractLabelsIdeal encoded count seed

A sampling law for re-encoded observations transports the ideal extraction experiment.

theorem Cslib.Crypto.Pseudoentropy.extractLabelsIdeal_map_snd {Observation Seed Output : Type} [Fintype Output] [Nonempty Output] (source : ProbComp Observation) (count : ℕ) (seed : ProbComp Seed) : PMF.map Prod.snd (extractLabelsIdeal source count seed) = seed.eval.bind fun (key : Seed) => PMF.map (fun (x : Output) => (key, x)) (Probability.PMF.uniformOfFintype Output)

Forgetting side information leaves an independent public seed and uniform output.

theorem Cslib.Crypto.Pseudoentropy.extractLabels_map_pair {α β Label Value Seed Output : Type} (observe : α → β) (encode : Label → Value) (seed : ProbComp Seed) (hash : Seed → List Value → Output) (samples : List (α × Label)) : extractLabels seed hash (List.map (fun (sample : α × Label) => (observe sample.1, encode sample.2)) samples) = (fun (result : List α × Seed × Output) => (List.map observe result.1, result.2)) <$> extractLabels seed (fun (key : Seed) (values : List Label) => hash key (List.map encode values)) samples

Re-encoding both fields changes only the hash's input representation and public output.

theorem Cslib.Crypto.Pseudoentropy.eval_replicate_extractLabels_map_pair {α β Label Value Seed Output : Type} (observe : α → β) (encode : Label → Value) (source : ProbComp (α × Label)) (count : ℕ) (seed : ProbComp Seed) (hash : Seed → List Value → Output) {encoded : ProbComp (β × Value)} (hsource : encoded.eval = PMF.map (fun (sample : α × Label) => (observe sample.1, encode sample.2)) source.eval) : (OracleComp.replicate count encoded >>= extractLabels seed hash).eval = PMF.map (fun (result : List α × Seed × Output) => (List.map observe result.1, result.2)) (OracleComp.replicate count source >>= extractLabels seed fun (key : Seed) (values : List Label) => hash key (List.map encode values)).eval

A sampling law for re-encoded observations and hash inputs transports the full repeated experiment. Only the output distribution matters; the sampler need not be a syntactic map.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_extractLabels {Param Observation Seed Output : Type} {input : Param ↪ List Bool} {observation : Observation ↪ List Bool} {key : Seed ↪ List Bool} {output : Output ↪ List Bool} {seed : Param → ProbComp Seed} {hash : Param → Seed → List Bool → Output} {samples : Param → List (Observation × Bool)} (hseed : Probability.IsPPTOn input key seed) (hhash : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : (Param × Seed) × List Bool) => hash pair.1.1 pair.1.2 pair.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input key) Turing.MultiTapeTM.encBits) output) (hsamples : Turing.MultiTapeTM.ComputableTidilyInPolyTime samples input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair observation Turing.MultiTapeTM.encBool))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList observation) (Turing.MultiTapeTM.encPair key output)) fun (a : Param) => extractLabels (seed a) (hash a) (samples a)

Label extraction composes ordinary sampling, list projections, and an efficient hash.

theorem Cslib.Crypto.Pseudoentropy.isPPTOn_extractLabels_list {Param Observation Label Seed Output : Type} {input : Param ↪ List Bool} {observation : Observation ↪ List Bool} {label : Label ↪ List Bool} {key : Seed ↪ List Bool} {output : Output ↪ List Bool} {seed : Param → ProbComp Seed} {hash : Param → Seed → List Label → Output} {samples : Param → List (Observation × Label)} (hseed : Probability.IsPPTOn input key seed) (hhash : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : (Param × Seed) × List Label) => hash pair.1.1 pair.1.2 pair.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair input key) (Turing.MultiTapeTM.encList label)) output) (hsamples : Turing.MultiTapeTM.ComputableTidilyInPolyTime samples input (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair observation label))) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encList observation) (Turing.MultiTapeTM.encPair key output)) fun (a : Param) => extractLabels (seed a) (hash a) (samples a)

Arbitrary encoded labels use the same extractor, with list encoding charged to the hash.

theorem Cslib.Crypto.Pseudoentropy.eval_replicate_extractLabels {Observation Label Seed Output : Type} [Finite Observation] [Finite Label] (source : ProbComp (Observation × Label)) (count : ℕ) (seed : ProbComp Seed) (hash : Seed → List Label → Output) : (OracleComp.replicate count source >>= extractLabels seed hash).eval = PMF.map (fun (result : (Fin count → Observation) × Seed × Output) => (List.ofFn result.1, result.2)) ((Probability.PMF.pi fun (x : Fin count) => source.eval).bind fun (outcome : Fin count → Observation × Label) => PMF.map (fun (s : Seed) => (fun (i : Fin count) => (outcome i).1, s, hash s (List.ofFn fun (i : Fin count) => (outcome i).2))) seed.eval)

Repeated program sampling and list-based extraction have the finite product experiment's exact law. Only the representation of the observation tuple changes.

theorem Cslib.Crypto.Pseudoentropy.extractLabels_sequence_gap {Observation Label Seed Output : Type} (original comparison : ProbComp (Observation × Label)) (count : ℕ) (seed : ProbComp Seed) (hash : Seed → List Label → Output) (test : List Observation × Seed × Output → ProbComp Bool) (ideal : PMF (List Observation × Seed × Output)) {ε : ℝ} (hclose : ↑(Game.advantage ((OracleComp.replicate count comparison >>= extractLabels seed hash).eval.bind fun (output : List Observation × Seed × Output) => (test output).eval) (ideal.bind fun (output : List Observation × Seed × Output) => (test output).eval)) ≤ ε) : have reduced := fun (samples : List (Observation × Label)) => extractLabels seed hash samples >>= test; ↑(Game.advantage (OracleComp.replicate count original >>= reduced).eval (ideal.bind fun (output : List Observation × Seed × Output) => (test output).eval)) - ε ≤ ↑(Game.advantage (OracleComp.replicate count original >>= reduced).eval (OracleComp.replicate count comparison >>= reduced).eval)

Extraction error for the supplied test is the only loss when converting its distinguishing advantage into a gap between original and comparison sample sequences. The hash seed is public.

theorem Cslib.Crypto.Pseudoentropy.extractLabels_dist_bind_le {Observation Label Seed Output : Type} [Finite Observation] [Finite Label] [Fintype Seed] [Fintype Output] [Nonempty Output] (source : ProbComp (Observation × Label)) (count informationBits : ℕ) (hsource : ∀ pair ∈ source.eval.support, 2 ^ (-↑informationBits) ≤ (source.eval pair).toReal) (seed : ProbComp Seed) (hash : Seed → List Label → Output) (hhash : Probability.IsTwoUniversal seed.eval fun (s : Seed) (bits : Fin count → Label) => hash s (List.ofFn bits)) {δ slack : ℝ} (hentropy : δ ≤ Probability.PMF.conditionalEntropy source.eval) (hslack : 0 ≤ slack) {Result : Type u_1} [Fintype Result] (test : List Observation × Seed × Output → PMF Result) : dist ((OracleComp.replicate count source >>= extractLabels seed hash).eval.bind test) ((extractLabelsIdeal (Prod.fst <$> source) count seed).bind test) ≤ 2 * Real.exp (-2 * slack ^ 2 / (↑count * ↑informationBits ^ 2)) + √(↑(Fintype.card Output) * (2 * 2 ^ (-(↑count * δ - slack)))) / 2

The list-based extractor inherits the conditional Shannon-entropy bound for repeated samples against every randomized finite-output test. The test receives all observations and the independent seed. It has no efficiency restriction.

theorem Cslib.Crypto.Pseudoentropy.eval_extractLabels_of_subsingleton {Observation Label Seed Output : Type} [Fintype Output] [Nonempty Output] [Subsingleton Output] (source : ProbComp (Observation × Label)) (count : ℕ) (seed : ProbComp Seed) (hash : Seed → List Label → Output) : (OracleComp.replicate count source >>= extractLabels seed hash).eval = extractLabelsIdeal (Prod.fst <$> source) count seed

Extracting into a singleton is exactly ideal, including its public observations and seed. This handles a zero-bit component without requiring a positive entropy budget.

theorem Cslib.Crypto.Pseudoentropy.extractLabels_indistinguishable {Observation Label Seed : ℕ → Type} [∀ (n : ℕ), Finite (Observation n)] [∀ (n : ℕ), Finite (Label n)] [(n : ℕ) → Fintype (Seed n)] (source : (n : ℕ) → ProbComp (Observation n × Label n)) (sourceBits inverseSlack outputBits : ℕ → ℕ) (hmass : ∀ (n : ℕ), ∀ value ∈ (source n).eval.support, 2 ^ (-↑(sourceBits n)) ≤ ((source n).eval value).toReal) (seed : (n : ℕ) → ProbComp (Seed n)) (hash : (n : ℕ) → Seed n → List (Label n) → BitString (outputBits n)) (hhash : ∀ (n : ℕ), Probability.IsTwoUniversal (seed n).eval fun (key : Seed n) (values : Fin (ExtractionSchedule.count n (sourceBits n) (inverseSlack n)) → Label n) => hash n key (List.ofFn values)) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, outputBits n = 0 ∨ ↑(outputBits n) + 2 * ↑(ExtractionSchedule.slack n (sourceBits n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (sourceBits n) (inverseSlack n)) * Probability.PMF.conditionalEntropy (source n).eval) : Game.Indistinguishable (fun (test : (n : ℕ) → List (Observation n) × Seed n × BitString (outputBits n) → Game) (n : ℕ) => (OracleComp.replicate (ExtractionSchedule.count n (sourceBits n) (inverseSlack n)) (source n) >>= extractLabels (seed n) (hash n)).eval.bind (test n)) (fun (test : (n : ℕ) → List (Observation n) × Seed n × BitString (outputBits n) → Game) (n : ℕ) => (extractLabelsIdeal (Prod.fst <$> source n) (ExtractionSchedule.count n (sourceBits n) (inverseSlack n)) (seed n)).bind (test n)) fun (x : (n : ℕ) → List (Observation n) × Seed n × BitString (outputBits n) → Game) => True

A shared repetition schedule makes conditional extraction statistically uniform. A zero-bit output is always permitted; positive lengths reserve two slacks below conditional entropy. Every randomized Boolean test is admissible, with no computability assumption on entropy or its numerical bound.

theorem Cslib.Crypto.Pseudoentropy.seededHash_replicate_indistinguishable {Label Seed : ℕ → Type} [∀ (n : ℕ), Finite (Label n)] [(n : ℕ) → Fintype (Seed n)] (source : (n : ℕ) → ProbComp (Label n)) (sourceBits inverseSlack outputBits : ℕ → ℕ) (hmass : ∀ (n : ℕ), ∀ value ∈ (source n).eval.support, 2 ^ (-↑(sourceBits n)) ≤ ((source n).eval value).toReal) (seed : (n : ℕ) → ProbComp (Seed n)) (hash : (n : ℕ) → Seed n → List (Label n) → BitString (outputBits n)) (hhash : ∀ (n : ℕ), Probability.IsTwoUniversal (seed n).eval fun (key : Seed n) (values : Fin (ExtractionSchedule.count n (sourceBits n) (inverseSlack n)) → Label n) => hash n key (List.ofFn values)) (hbudget : ∀ᶠ (n : ℕ) in Filter.atTop, outputBits n = 0 ∨ ↑(outputBits n) + 2 * ↑(ExtractionSchedule.slack n (sourceBits n) (inverseSlack n)) ≤ ↑(ExtractionSchedule.count n (sourceBits n) (inverseSlack n)) * Probability.PMF.entropy (source n).eval) : Game.Indistinguishable (fun (test : (n : ℕ) → Seed n × BitString (outputBits n) → Game) (n : ℕ) => (Probability.seededHash (seed n).eval (ProbComp.eval (OracleComp.replicate (ExtractionSchedule.count n (sourceBits n) (inverseSlack n)) (source n))) (hash n)).bind (test n)) (fun (test : (n : ℕ) → Seed n × BitString (outputBits n) → Game) (n : ℕ) => do let key ← (seed n).eval let result ← PMF.map (fun (x : BitString (outputBits n)) => (key, x)) (Probability.PMF.uniformOfFintype (BitString (outputBits n))) test n result) fun (x : (n : ℕ) → Seed n × BitString (outputBits n) → Game) => True

Unconditional extraction is the constant-observation specialization. It hashes ordinary lists and reveals the entire seed; zero-bit outputs need no entropy.