Correctness of the clocked boosting loop

The potential invariant refers to the predictor descriptions stored by the executable program. Its active branch records density restoration and accumulated potential decrease. Its stopped branch records the error of the executable majority predictor. Weighted correlation for the learner's truncated output remains an explicit hypothesis; implementing the learner and its security reduction is separate work.

Main definitions

• State.GoodPredictor: weighted correlation of the truncated description actually stored.
• State.Invariant, State.Successful: potential progress and the final prediction guarantee.

Main results

• round_sound, run_invariant: local test and learner errors accumulate additively.
• run_sound: a majority-or-dense-margin guarantee under the learner contract.

References

[Hol05], Section 2.2, Figure 2, Claims 2.7, 2.10–2.13, 2.16, and Lemma 2.14. The proved clock replaces the worst-dense-set stopping test. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid (params : Parameters) : Prop

The rational density lies in (0, 1]. Invalid parameters still define a terminating program.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.delta (params : Parameters) : ℝ

The density represented by the integer parameters.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.rate (params : Parameters) : ℝ

The slope used by the dyadic weight sampler.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.gamma (params : Parameters) : ℝ

The correlation required of the learner, so that gamma * delta = rate.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.denominator_pos (params : Parameters) : 0 < params.denominator

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.inverseRate_pos (params : Parameters) : 0 < params.inverseRate

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.rate_pos (params : Parameters) : 0 < params.rate

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.delta_pos {params : Parameters} (h : params.Valid) : 0 < params.delta

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.delta_le_one {params : Parameters} (h : params.Valid) : params.delta ≤ 1

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.gamma_pos {params : Parameters} (h : params.Valid) : 0 < params.gamma

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.gamma_mul_delta {params : Parameters} (h : params.Valid) : params.gamma * params.delta = params.rate

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.inverse_delta {params : Parameters} (h : params.Valid) : 1 ≤ ↑params.denominator * params.delta

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.inverse_gamma {params : Parameters} (h : params.Valid) : 1 ≤ ↑params.inverseRate * params.gamma

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.majority_precision {params : Parameters} (h : params.Valid) : 1 / ↑params.majorityPrecision ≤ params.delta / 32

The executable sampling precision meets the majority guard's tolerance.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.shift_precision {params : Parameters} (h : params.Valid) : 1 / ↑params.shiftPrecision ≤ params.delta * params.rate / 32

The executable sampling precision meets the density guard's tolerance.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.clock_budget {params : Parameters} (h : params.Valid) : 1 / (2 * params.rate) ≤ ↑params.clock * (params.gamma * params.delta ^ 2 / 8)

The integer clock pays for the initial potential, including equality at the boundary.

def Cslib.Crypto.Pseudoentropy.Boosting.State.margin {α : Type u_1} (state : State) (predict : List Bool → α → Bool) (truth : α → Bool) (x : α) : ℝ

The signed margin of the stored descriptions on a labeled source point.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.margin_initial {α : Type u_1} (predict : List Bool → α → Bool) (truth : α → Bool) (x : α) : initial.margin predict truth x = 0

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.margin_shift {α : Type u_1} (state : State) (yes : Bool) (predict : List Bool → α → Bool) (truth : α → Bool) (x : α) : (state.shift yes).margin predict truth x = state.margin predict truth x

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.margin_add {α : Type u_1} (state : State) (bound : ℕ) (code : List Bool) (predict : List Bool → α → Bool) (truth : α → Bool) (x : α) : (state.add bound code).margin predict truth x = state.margin predict truth x + BitString.signedVote (predict (List.take bound code) x) (truth x)

def Cslib.Crypto.Pseudoentropy.Boosting.State.GoodPredictor {α : Type u_1} [Fintype α] (source : PMF α) (predict : List Bool → α → Bool) (truth : α → Bool) (params : Parameters) (state : State) (code : List Bool) : Prop

The learner's obligation is weighted correlation of the description actually stored.

def Cslib.Crypto.Pseudoentropy.Boosting.State.Invariant {α : Type u_1} [Fintype α] (source : PMF α) (predict : List Bool → α → Bool) (truth : α → Bool) (params : Parameters) (rounds : ℕ) (state : State) : Prop

A good state either has small majority error or records all progress so far. The extra unit of shift in the density clause allows the next round to restore density.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.invariant_initial {α : Type u_1} [Fintype α] (source : PMF α) (predict : List Bool → α → Bool) (truth : α → Bool) (params : Parameters) (hparams : params.Valid) : Invariant source predict truth params 0 initial

Before any predictors, the density is full and the potential equals its initial budget.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.invariant_stop {α : Type u_1} [Fintype α] (source : PMF α) (predict : List Bool → α → Bool) (truth : α → Bool) (params : Parameters) (rounds : ℕ) (state : State) (herror : (source.toOuterMeasure {x : α | BitString.listStrictMajority (List.map (fun (code : List Bool) => predict code x) state.predictors) ≠ truth x}).toReal ≤ 7 * params.delta / 16) : Invariant source predict truth params rounds { stopped := true, threshold := state.threshold, predictors := state.predictors }

A valid stopping decision establishes the stopped branch for every subsequent round.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.Invariant.shift_add {α : Type u_1} [Fintype α] (source : PMF α) (predict : List Bool → α → Bool) (truth : α → Bool) (params : Parameters) {rounds : ℕ} {state : State} (hstate : Invariant source predict truth params rounds state) (hparams : params.Valid) (hactive : state.stopped = false) (yes : Bool) (code : List Bool) (hguard : if yes = true then (density source params.rate fun (x : α) => state.margin predict truth x - ↑state.threshold) ≤ params.delta * (1 + params.rate / 16) else params.delta ≤ density source params.rate fun (x : α) => state.margin predict truth x - ↑state.threshold) (hbelow : 3 * params.delta / 8 ≤ (source.toOuterMeasure {x : α | state.margin predict truth x ≤ 0}).toReal) (hcorrelation : GoodPredictor source predict truth params (state.shift yes) code) : Invariant source predict truth params (rounds + 1) ((state.shift yes).add params.codeBound code)

One valid shift decision and one correlated predictor maintain the analytic invariant. All margins here are computed from the program's stored descriptions.

def Cslib.Crypto.Pseudoentropy.Boosting.State.Successful {α : Type u_1} [Fintype α] (source : PMF α) (predict : List Bool → α → Bool) (truth : α → Bool) (params : Parameters) (state : State) : Prop

At the clock, the program has either a good majority predictor or a collection with large average signed margin on every dense soft set. The latter is the input to the clipped-vote step.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.Invariant.successful {α : Type u_1} [Fintype α] (source : PMF α) (predict : List Bool → α → Bool) (truth : α → Bool) (params : Parameters) {state : State} (hstate : Invariant source predict truth params params.clock state) (hparams : params.Valid) : Successful source predict truth params state

The same invariant that follows the program proves its clock-boundary guarantee.

theorem Cslib.Crypto.Pseudoentropy.Boosting.round_sound {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (learn : State → ProbComp (List Bool)) (params : Parameters) (hparams : params.Valid) {error : ℝ} (herror : 0 ≤ error) {rounds : ℕ} {state : State} (hstate : State.Invariant source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params rounds state) (hlearn : ∀ (yes : Bool), (params.delta ≤ density source.eval params.rate fun (x : α) => (state.shift yes).margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth x - ↑(state.shift yes).threshold) → ((learn (state.shift yes)).eval.toOuterMeasure {code : List Bool | ¬State.GoodPredictor source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params (state.shift yes) code}).toReal ≤ error) : ((round evaluate ((fun (x : α) => (observe x, truth x)) <$> source) learn params state).eval.toOuterMeasure {next : State | ¬State.Invariant source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params (rounds + 1) next}).toReal ≤ 2 * (1 / 2) ^ params.confidence + error

A sampled round preserves the potential invariant except for its two test errors and the learner's stated error. The learner need only succeed when the shifted measure is dense.

theorem Cslib.Crypto.Pseudoentropy.Boosting.run_invariant {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (learn : State → ProbComp (List Bool)) (params : Parameters) (hparams : params.Valid) {error : ℝ} (herror : 0 ≤ error) (hlearn : ∀ (state : State), (params.delta ≤ density source.eval params.rate fun (x : α) => state.margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth x - ↑state.threshold) → ((learn state).eval.toOuterMeasure {code : List Bool | ¬State.GoodPredictor source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state code}).toReal ≤ error) : ((run evaluate ((fun (x : α) => (observe x, truth x)) <$> source) learn params).eval.toOuterMeasure {state : State | ¬State.Invariant source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params params.clock state}).toReal ≤ ↑params.clock * (2 * (1 / 2) ^ params.confidence + error)

Adaptive choices incur only the sum of the local errors, with no independence assumption between rounds. Stopped states keep their majority guarantee for the remaining clock ticks.

theorem Cslib.Crypto.Pseudoentropy.Boosting.run_sound {α : Type} [Fintype α] (source : ProbComp α) (observe : α → List Bool) (truth : α → Bool) (evaluate : List Bool → List Bool → Bool) (learn : State → ProbComp (List Bool)) (params : Parameters) (hparams : params.Valid) {error : ℝ} (herror : 0 ≤ error) (hlearn : ∀ (state : State), (params.delta ≤ density source.eval params.rate fun (x : α) => state.margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth x - ↑state.threshold) → ((learn state).eval.toOuterMeasure {code : List Bool | ¬State.GoodPredictor source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state code}).toReal ≤ error) : ((run evaluate ((fun (x : α) => (observe x, truth x)) <$> source) learn params).eval.toOuterMeasure {state : State | ¬State.Successful source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state}).toReal ≤ ↑params.clock * (2 * (1 / 2) ^ params.confidence + error)

The executable loop produces the majority-or-dense-margin guarantee, except with its explicit total error. The learner contract remains a hypothesis. Combining this with a certified learner and the final clipped-vote predictor is a separate development.