Documentation

Complexity.Crypto.Computational.Pseudoentropy.DenseMask

Dense masks against uniform sequence tests #

A pseudoentropy pair's prediction bound forces every efficient sequence test to admit a dense soft mask with small distinguishing gap. Otherwise the concrete sequence learner constructs one uniform strict PPT predictor violating that bound. The mask's nonzero probabilities have an explicit inverse-polynomial lower bound, needed for the subsequent extraction estimate.

The density and repetition schedules are efficiently computable. The indexed theorem gives one eventual threshold for every member of a polynomial-size family of tests and density numerators. The density need only be valid and below the entropy threshold where the conclusion is used. Neither the program nor its parameters are chosen separately at each input length.

Main results #

References #

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_exists_indexed_mask {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (test : ℕ → ℕ → List (List Bool × Bool) → ProbComp Bool) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool fun (input : (ℕ × ℕ) × List (List Bool × Bool)) => test input.1.1 input.1.2 input.2) {candidates count densityBound inverseGap : ℕ → ℕ} {numerator : ℕ → ℕ → ℕ} (hcandidates : Turing.MultiTapeTM.ComputableTidilyInPolyTime candidates Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (input : ℕ × ℕ) => numerator input.1 input.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hinverseGap : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseGap Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hgap : ∀ (n : ℕ), 0 < inverseGap n) :
∀ᶠ (n : ℕ) in Filter.atTop, ∀ i < candidates n, 0 < numerator n i → numerator n i ≤ Probability.dyadicSize (densityBound n) → ↑(numerator n i) / ↑(Probability.dyadicSize (densityBound n)) ≤ Probability.PMF.conditionalEntropy (pair.joint n) + gap n → ∃ (mask : pair.Observation n × Bool → ProbComp Bool), ↑(numerator n i) / ↑(Probability.dyadicSize (densityBound n)) ≤ ((pair.latentSample n >>= mask).eval true).toReal ∧ (∀ (value : pair.Observation n × Bool), 0 < ((mask value).eval true).toReal → 1 / ↑(Probability.dyadicSize (2 * inverseGap n * Probability.dyadicSize (densityBound n))) ≤ ((mask value).eval true).toReal) ∧ ↑(Game.advantage (OracleComp.replicate (count n) (pair.sample n) >>= test n i).eval (OracleComp.replicate (count n) (maskedSample (pair.latentSample n) (fun (value : pair.Observation n × Bool) => (pair.encode n) value.1) Prod.snd mask) >>= test n i).eval) < ↑(Probability.dyadicSize (count n)) / ↑(inverseGap n)

All tests in a uniformly efficient polynomial-size family eventually admit dense soft masks with small distinguishing gap whenever their density is valid. The common eventual threshold allows arbitrary choices of index in the proof without supplying that choice to the program.

theorem Cslib.Crypto.Pseudoentropy.SamplablePair.HasGap.eventually_exists_mask {pair : SamplablePair} {gap : ℕ → ℝ} (hpair : pair.HasGap gap) (test : ℕ → List (List Bool × Bool) → ProbComp Bool) (htest : Probability.IsPPTOn (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool))) Turing.MultiTapeTM.encBool fun (input : ℕ × List (List Bool × Bool)) => test input.1 input.2) {count numerator densityBound inverseGap : ℕ → ℕ} (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime numerator Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hdensity : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hinverseGap : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseGap Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hgap : ∀ (n : ℕ), 0 < inverseGap n) :
∀ᶠ (n : ℕ) in Filter.atTop, 0 < numerator n → numerator n ≤ Probability.dyadicSize (densityBound n) → ↑(numerator n) / ↑(Probability.dyadicSize (densityBound n)) ≤ Probability.PMF.conditionalEntropy (pair.joint n) + gap n → ∃ (mask : pair.Observation n × Bool → ProbComp Bool), ↑(numerator n) / ↑(Probability.dyadicSize (densityBound n)) ≤ ((pair.latentSample n >>= mask).eval true).toReal ∧ (∀ (value : pair.Observation n × Bool), 0 < ((mask value).eval true).toReal → 1 / ↑(Probability.dyadicSize (2 * inverseGap n * Probability.dyadicSize (densityBound n))) ≤ ((mask value).eval true).toReal) ∧ ↑(Game.advantage (OracleComp.replicate (count n) (pair.sample n) >>= test n).eval (OracleComp.replicate (count n) (maskedSample (pair.latentSample n) (fun (value : pair.Observation n × Bool) => (pair.encode n) value.1) Prod.snd mask) >>= test n).eval) < ↑(Probability.dyadicSize (count n)) / ↑(inverseGap n)

Every uniform sequence test eventually admits a dense soft mask with small distinguishing gap. The mask may depend on the test and parameter; its positive probabilities are uniformly bounded below by the configured dyadic rate. The statement exposes no boosting state.