Sampling the soft weights of hard-core boosting

Votes are ordinary Boolean words. The number of correct votes, the threshold, and the dyadic rate determine a natural-number numerator. Saturating subtraction implements both clipped regions of the real weight curve; neither real arithmetic nor rejection sampling is needed. isPPTOn_sampleWeight certifies the whole program through the shared programming combinators. sampleWeight_density_deviation estimates the source-averaged density with a Hoeffding bound, using a natural success counter and independent source examples.

Each call draws a fresh coin. An implementation of a random set must additionally cache answers to repeated membership queries; this program alone is not such a stateful oracle.

Main definitions

• Cslib.Crypto.Pseudoentropy.Boosting.weightNumerator: clipped dyadic weights using naturals.
• Cslib.Crypto.Pseudoentropy.Boosting.sampleWeight: a fresh exact weight coin.

Main results

• Cslib.Crypto.Pseudoentropy.Boosting.eval_sampleWeight_true: exact agreement with the weight.
• Cslib.Crypto.Pseudoentropy.Boosting.sampleWeight_density_deviation: density concentration.
• Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_sampleWeight: the uniform strict PPT certificate.

References

Holenstein, Section 2.2, Figure 1 and Claims 2.6–2.8. Adapted from Crypto/Computational/Pseudoentropy/Boosting/Sampling.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, with typed tidy-machine certificates.

def Cslib.Crypto.Pseudoentropy.Boosting.weightNumerator (denominator rateNumerator threshold : ℕ) (votes : List Bool) (truth : Bool) : ℕ

The numerator of a clipped linear weight, computed entirely with natural numbers. The excess of correct over incorrect votes is 2 * votes.count truth - votes.length in integer arithmetic; the inner natural subtraction keeps only its excess over the threshold.

theorem Cslib.Crypto.Pseudoentropy.Boosting.weightNumerator_le (denominator rateNumerator threshold : ℕ) (votes : List Bool) (truth : Bool) : weightNumerator denominator rateNumerator threshold votes truth ≤ denominator

Every generated numerator is within its denominator, including malformed parameter choices.

theorem Cslib.Crypto.Pseudoentropy.Boosting.weightNumerator_div (denominator rateNumerator threshold : ℕ) (hdenominator : 0 < denominator) (votes : List Bool) (truth : Bool) : ↑(weightNumerator denominator rateNumerator threshold votes truth) / ↑denominator = weight (↑rateNumerator / ↑denominator) (BitString.listVoteMargin votes truth - ↑threshold)

Saturating natural arithmetic exactly implements the clipped real-valued weight curve.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPolyTime_weightNumerator {α : Type} {input : α ↪ List Bool} {denominator rateNumerator threshold : α → ℕ} {votes : α → List Bool} {truth : α → Bool} (hdenominator : Turing.MultiTapeTM.ComputableTidilyInPolyTime denominator input Turing.MultiTapeTM.encUnary) (hrate : Turing.MultiTapeTM.ComputableTidilyInPolyTime rateNumerator input Turing.MultiTapeTM.encUnary) (hthreshold : Turing.MultiTapeTM.ComputableTidilyInPolyTime threshold input Turing.MultiTapeTM.encUnary) (hvotes : Turing.MultiTapeTM.ComputableTidilyInPolyTime votes input Turing.MultiTapeTM.encBits) (htruth : Turing.MultiTapeTM.ComputableTidilyInPolyTime truth input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => weightNumerator (denominator a) (rateNumerator a) (threshold a) (votes a) (truth a)) input Turing.MultiTapeTM.encUnary

The weight's natural numerator is polynomial time in its complete encoded input.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.sampleWeight (bound rateNumerator threshold : ℕ) (votes : List Bool) (truth : Bool) : ProbComp Bool

Sample a fresh membership coin with the soft weight of this vote word.

theorem Cslib.Crypto.Pseudoentropy.Boosting.eval_sampleWeight_true (bound rateNumerator threshold : ℕ) (votes : List Bool) (truth : Bool) : ((sampleWeight bound rateNumerator threshold votes truth).eval true).toReal = weight (↑rateNumerator / ↑(Probability.dyadicSize bound)) (BitString.listVoteMargin votes truth - ↑threshold)

The program's acceptance probability is exactly the soft weight used in the potential proof.

theorem Cslib.Crypto.Pseudoentropy.Boosting.sampleWeight_density {α : Type u_1} [Fintype α] (source : PMF α) (bound rateNumerator threshold : ℕ) (votes : α → List Bool) (truth : α → Bool) : ((source.bind fun (x : α) => (sampleWeight bound rateNumerator threshold (votes x) (truth x)).eval) true).toReal = density source (↑rateNumerator / ↑(Probability.dyadicSize bound)) fun (x : α) => BitString.listVoteMargin (votes x) (truth x) - ↑threshold

Sampling a source example and then its weight coin accepts with exactly the soft density.

theorem Cslib.Crypto.Pseudoentropy.Boosting.sampleWeight_density_deviation {α : Type} [Fintype α] (source : ProbComp α) (bound rateNumerator threshold : ℕ) (votes : α → List Bool) (truth : α → Bool) (count : ℕ) (hcount : 0 < count) {ε : ℝ} (hε : 0 ≤ ε) : ((ProbComp.eval (OracleComp.countTrue count do let x ← source sampleWeight bound rateNumerator threshold (votes x) (truth x))).toOuterMeasure {successes : ℕ | ε ≤ |↑successes / ↑count - density source.eval (↑rateNumerator / ↑(Probability.dyadicSize bound)) fun (x : α) => BitString.listVoteMargin (votes x) (truth x) - ↑threshold|}).toReal ≤ 2 * Real.exp (-2 * ↑count * ε ^ 2)

Repeated source examples and fresh weight coins estimate the soft density. The executable counter uses natural numbers; the empirical fraction occurs only in its specification.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_sampleWeight {α : Type} {input : α ↪ List Bool} {bound rateNumerator threshold : α → ℕ} {votes : α → List Bool} {truth : α → Bool} (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hrate : Turing.MultiTapeTM.ComputableTidilyInPolyTime rateNumerator input Turing.MultiTapeTM.encUnary) (hthreshold : Turing.MultiTapeTM.ComputableTidilyInPolyTime threshold input Turing.MultiTapeTM.encUnary) (hvotes : Turing.MultiTapeTM.ComputableTidilyInPolyTime votes input Turing.MultiTapeTM.encBits) (htruth : Turing.MultiTapeTM.ComputableTidilyInPolyTime truth input Turing.MultiTapeTM.encBool) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => sampleWeight (bound a) (rateNumerator a) (threshold a) (votes a) (truth a)

Runtime-dependent parameters, votes, and labels compose to a uniform strict PPT sampler.