Repeated extraction with an executable matrix hash #
The three extractors in the pseudoentropy construction share this program. A client prepares the label list as one word; the extractor supplies a fresh matrix, hashes at the declared width, and retains every observation and the complete matrix seed. Width normalization specifies total behavior on malformed inputs without affecting the finite extraction laws.
Main definitions #
extractMatrixLabels: retain observations while hashing normalized labels with a fresh matrix.extractMatrixLabelsIdeal: the independent comparison program with the same public seed.
Main results #
isPPTOn_extractMatrixLabels: certify sampling, hashing and copying at runtime dimensions.eval_extractMatrixLabels: the exact finite matrix experiment.eval_extractMatrixLabelsIdeal_append: combine the ideal seed and digest after any processing of the public observations.
References #
- Thomas Holenstein, Pseudorandom Generators from One-Way Functions: A Simple Construction for Any Hardness, TCC 2006, Section 5. [Hol06]. We use the shared Boolean-matrix family in place of finite-field hashing.
Adapted from the cslib crypto branch at
5ff69ca93402e7c947208dc56396d6d86203ccd8.
theorem Cslib.Crypto.Pseudoentropy.extractMatrixLabels_result {Observation Label : Type} (inputBits outputBits : ℕ) (prepare : List Label → List Bool) (samples : List (Observation × Label)) {result : List Observation × List Bool × List Bool} (hresult : result ∈ (extractMatrixLabels inputBits outputBits prepare samples).eval.support) :
Every result preserves the observations and has the declared seed and digest lengths.
noncomputable def Cslib.Crypto.Pseudoentropy.extractMatrixLabelsIdeal {Observation : Type} (source : ProbComp Observation) (count inputBits outputBits : ℕ) :
The comparison experiment preserves the observations and samples independent seed and bits.
Instances For
theorem Cslib.Crypto.Pseudoentropy.isPPTOn_extractMatrixLabels {α Observation Label : Type} {input : α ↪ List Bool} {observation : Observation ↪ List Bool} {label : Label ↪ List Bool} {inputBits outputBits : α → ℕ} {prepare : α → List Label → List Bool} {samples : α → List (Observation × Label)} (hinput : Turing.MultiTapeTM.ComputableTidilyInPolyTime inputBits input Turing.MultiTapeTM.encUnary) (houtput : Turing.MultiTapeTM.ComputableTidilyInPolyTime outputBits input Turing.MultiTapeTM.encUnary) (hprepare :
Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : α × List Label) => prepare pair.1 pair.2)
(Turing.MultiTapeTM.encPair input (Turing.MultiTapeTM.encList label)) Turing.MultiTapeTM.encBits) (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 Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits))
fun (a : α) => extractMatrixLabels (inputBits a) (outputBits a) (prepare a) (samples a)
Runtime dimensions and a certified preparation function give an ordinary PPT program.
theorem Cslib.Crypto.Pseudoentropy.eval_extractMatrixLabels {Observation Label : Type} (inputBits outputBits : ℕ) (prepare : List Label → List Bool) (samples : List (Observation × Label)) :
(extractMatrixLabels inputBits outputBits prepare samples).eval = PMF.map
(fun (result : List Observation × BitString (outputBits * inputBits) × BitString outputBits) =>
(result.1, List.ofFn result.2.1, List.ofFn result.2.2))
(extractLabels (ProbComp.uniform (BitString (outputBits * inputBits)))
(fun (seed : BitString (outputBits * inputBits)) (labels : List Label) =>
BitString.LinearHash.hash (BitString.blocksEquiv seed) (BitString.ofList inputBits (prepare labels)))
samples).eval
Word matrix sampling and hashing exactly realize the finite extraction experiment.
theorem Cslib.Crypto.Pseudoentropy.eval_extractMatrixLabelsIdeal {Observation : Type} (source : ProbComp Observation) (count inputBits outputBits : ℕ) :
(extractMatrixLabelsIdeal source count inputBits outputBits).eval = PMF.map
(fun (result : List Observation × BitString (outputBits * inputBits) × BitString outputBits) =>
(result.1, List.ofFn result.2.1, List.ofFn result.2.2))
(extractLabelsIdeal source count (ProbComp.uniform (BitString (outputBits * inputBits))))
The ideal word program agrees with the finite ideal distribution, retaining the full seed.
theorem Cslib.Crypto.Pseudoentropy.eval_extractMatrixLabelsIdeal_bind {Observation Output : Type} (source : ProbComp Observation) (count inputBits outputBits : ℕ) (next : List Observation → List Bool → ProbComp Output) :
(do
let result ← extractMatrixLabelsIdeal source count inputBits outputBits
next result.1 (result.2.1 ++ result.2.2)).eval = (do
let observations ← OracleComp.replicate count source
let bits ← BitString.sampleList (outputBits * inputBits + outputBits)
next observations bits).eval
In the ideal experiment, the public matrix seed and digest together form one uniform word. The continuation may depend on all retained observations.
theorem Cslib.Crypto.Pseudoentropy.eval_extractMatrixLabelsIdeal_append {Observation : Type} (source : ProbComp Observation) (count inputBits outputBits : ℕ) (next : List Observation → ProbComp (List Bool)) :
(do
let result ← extractMatrixLabelsIdeal source count inputBits outputBits
(fun (front : List Bool) => front ++ (result.2.1 ++ result.2.2)) <$> next result.1).eval = (do
let observations ← OracleComp.replicate count source
let front ← next observations
let suffix ← BitString.sampleList (outputBits * inputBits + outputBits)
pure (front ++ suffix)).eval
An independently uniform ideal hash can be sampled after processing the observations.