Sampled decisions for uniform hard-core boosting

testShift estimates the soft density and decides whether to raise the threshold. testMajority estimates the probability of a nonpositive raw vote margin and decides whether the majority predictor is already good enough. Both tests use natural counts and rational cross-products, have strict PPT certificates, and meet the overlapping guards except with probability at most 2⁻ᵏ for confidence parameter k.

The trial programs are explicit inputs: they must sample fresh examples and evaluate the relevant weight or margin predicate. sampleWeight_density supplies the density correspondence. The collection's worst-dense-set stopping test is not implemented here; the finite boosting clock provides a separate route to a dense-margin guarantee at the final round.

Main definitions

• testShift, testMajority: rational tests of soft density and raw-margin error.

Main results

• testShift_weights_sound, testMajority_source_sound: guards for the boosting loop.
• isPPTOn_testShift, isPPTOn_testMajority: strict computational certificates.

References

[Hol05], Section 2.2, Figure 2 and Claim 2.6. The test thresholds are midpoints of the pairs of overlapping guards. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.Crypto.Pseudoentropy.Boosting.testShift (confidence inverseTolerance densityNumerator densityDenominator rateNumerator rateDenominator : ℕ) (trial : ProbComp Bool) : ProbComp Bool

Test whether the soft density is small enough to raise the vote threshold. With density parameter δ and weight rate η, the comparison threshold is δ (1 + η / 32).

def Cslib.Crypto.Pseudoentropy.Boosting.testMajority (confidence inverseTolerance densityNumerator densityDenominator : ℕ) (trial : ProbComp Bool) : ProbComp Bool

Test whether the nonpositive-margin probability is small enough to return the majority predictor. The threshold 13δ / 32 lies midway between 3δ / 8 and 7δ / 16.

theorem Cslib.Crypto.Pseudoentropy.Boosting.testShift_sound (confidence inverseTolerance densityNumerator densityDenominator rateNumerator rateDenominator : ℕ) (trial : ProbComp Bool) (htolerance : 0 < inverseTolerance) (hdensity : 0 < densityDenominator) (hrate : 0 < rateDenominator) (hprecision : 1 / ↑inverseTolerance ≤ ↑densityNumerator / ↑densityDenominator * (↑rateNumerator / ↑rateDenominator) / 32) : ((testShift confidence inverseTolerance densityNumerator densityDenominator rateNumerator rateDenominator trial).eval.toOuterMeasure {shift : Bool | ¬if shift = true then (trial.eval true).toReal ≤ ↑densityNumerator / ↑densityDenominator * (1 + ↑rateNumerator / ↑rateDenominator / 16) else ↑densityNumerator / ↑densityDenominator ≤ (trial.eval true).toReal}).toReal ≤ (1 / 2) ^ confidence

The sampled shift decision satisfies the density guards from Figure 2. Substituting rate = γδ gives the upper guard δ (1 + γδ / 16) used by step_progress.

theorem Cslib.Crypto.Pseudoentropy.Boosting.testMajority_sound (confidence inverseTolerance densityNumerator densityDenominator : ℕ) (trial : ProbComp Bool) (htolerance : 0 < inverseTolerance) (hdensity : 0 < densityDenominator) (hprecision : 1 / ↑inverseTolerance ≤ ↑densityNumerator / ↑densityDenominator / 32) : ((testMajority confidence inverseTolerance densityNumerator densityDenominator trial).eval.toOuterMeasure {stop : Bool | ¬if stop = true then (trial.eval true).toReal ≤ 7 * (↑densityNumerator / ↑densityDenominator) / 16 else 3 * (↑densityNumerator / ↑densityDenominator) / 8 ≤ (trial.eval true).toReal}).toReal ≤ (1 / 2) ^ confidence

The sampled majority decision satisfies the two majority guards from Figure 2.

theorem Cslib.Crypto.Pseudoentropy.Boosting.testMajority_source_sound {α : Type} (source : ProbComp α) (votes : α → List Bool) (truth : α → Bool) (confidence inverseTolerance densityNumerator densityDenominator : ℕ) (htolerance : 0 < inverseTolerance) (hdensity : 0 < densityDenominator) (hprecision : 1 / ↑inverseTolerance ≤ ↑densityNumerator / ↑densityDenominator / 32) : ((testMajority confidence inverseTolerance densityNumerator densityDenominator ((fun (x : α) => BitString.listNonpositiveMargin (votes x) (truth x)) <$> source)).eval.toOuterMeasure {stop : Bool | ¬if stop = true then (source.eval.toOuterMeasure {x : α | BitString.listStrictMajority (votes x) ≠ truth x}).toReal ≤ 7 * (↑densityNumerator / ↑densityDenominator) / 16 else 3 * (↑densityNumerator / ↑densityDenominator) / 8 ≤ (source.eval.toOuterMeasure {x : α | BitString.listVoteMargin (votes x) (truth x) ≤ 0}).toReal}).toReal ≤ (1 / 2) ^ confidence

When the trial draws an example and tests its votes, a valid stopping decision certifies the actual majority predictor. A valid continuation certifies the raw-margin lower guard.

theorem Cslib.Crypto.Pseudoentropy.Boosting.testShift_weights_sound {α : Type} [Fintype α] (source : ProbComp α) (votes : α → List Bool) (truth : α → Bool) (confidence inverseTolerance densityNumerator densityDenominator bound rateNumerator threshold : ℕ) (htolerance : 0 < inverseTolerance) (hdensity : 0 < densityDenominator) (hprecision : 1 / ↑inverseTolerance ≤ ↑densityNumerator / ↑densityDenominator * (↑rateNumerator / ↑(Probability.dyadicSize bound)) / 32) : ((testShift confidence inverseTolerance densityNumerator densityDenominator rateNumerator (Probability.dyadicSize bound) do let x ← source sampleWeight bound rateNumerator threshold (votes x) (truth x)).eval.toOuterMeasure {shift : Bool | ¬if shift = true then (density source.eval (↑rateNumerator / ↑(Probability.dyadicSize bound)) fun (x : α) => BitString.listVoteMargin (votes x) (truth x) - ↑threshold) ≤ ↑densityNumerator / ↑densityDenominator * (1 + ↑rateNumerator / ↑(Probability.dyadicSize bound) / 16) else ↑densityNumerator / ↑densityDenominator ≤ density source.eval (↑rateNumerator / ↑(Probability.dyadicSize bound)) fun (x : α) => BitString.listVoteMargin (votes x) (truth x) - ↑threshold}).toReal ≤ (1 / 2) ^ confidence

Fresh source examples and weight coins implement the density test used by the loop. This connects the executable decision directly to the density from the potential proof.

theorem Cslib.Crypto.Pseudoentropy.Boosting.majority_precision_of_inverse (inverseDensity : ℕ) {δ : ℝ} (hdensity : 1 ≤ ↑inverseDensity * δ) : 1 / ↑(32 * inverseDensity) ≤ δ / 32

A natural upper bound on inverse density gives a sufficient majority-test tolerance.

theorem Cslib.Crypto.Pseudoentropy.Boosting.shift_precision_of_inverse (inverseGamma inverseDensity : ℕ) {γ δ : ℝ} (hgamma : 1 ≤ ↑inverseGamma * γ) (hdensity : 1 ≤ ↑inverseDensity * δ) : 1 / ↑(32 * inverseGamma * inverseDensity ^ 2) ≤ δ * (γ * δ) / 32

Natural inverse bounds give a sufficient shift-test tolerance when the weight rate is γδ. The reciprocal precision and hence the number of trials remain polynomial in these bounds.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_testShift {α : Type} {input : α ↪ List Bool} {trial : α → ProbComp Bool} {confidence inverseTolerance densityNumerator densityDenominator rateNumerator rateDenominator : α → ℕ} (htrial : Probability.IsPPTOn input Turing.MultiTapeTM.encBool trial) (hconfidence : Turing.MultiTapeTM.ComputableTidilyInPolyTime confidence input Turing.MultiTapeTM.encUnary) (htolerance : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseTolerance input Turing.MultiTapeTM.encUnary) (hdensityNum : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityNumerator input Turing.MultiTapeTM.encUnary) (hdensityDen : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityDenominator input Turing.MultiTapeTM.encUnary) (hrateNum : Turing.MultiTapeTM.ComputableTidilyInPolyTime rateNumerator input Turing.MultiTapeTM.encUnary) (hrateDen : Turing.MultiTapeTM.ComputableTidilyInPolyTime rateDenominator input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => testShift (confidence a) (inverseTolerance a) (densityNumerator a) (densityDenominator a) (rateNumerator a) (rateDenominator a) (trial a)

Efficient trials and unary parameters give a strict PPT shift decision.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_testMajority {α : Type} {input : α ↪ List Bool} {trial : α → ProbComp Bool} {confidence inverseTolerance densityNumerator densityDenominator : α → ℕ} (htrial : Probability.IsPPTOn input Turing.MultiTapeTM.encBool trial) (hconfidence : Turing.MultiTapeTM.ComputableTidilyInPolyTime confidence input Turing.MultiTapeTM.encUnary) (htolerance : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseTolerance input Turing.MultiTapeTM.encUnary) (hdensityNum : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityNumerator input Turing.MultiTapeTM.encUnary) (hdensityDen : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityDenominator input Turing.MultiTapeTM.encUnary) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => testMajority (confidence a) (inverseTolerance a) (densityNumerator a) (densityDenominator a) (trial a)

Efficient trials and unary parameters give a strict PPT majority decision.