A clocked hard-core boosting program

The state stores a threshold, a list of predictor descriptions, and a stopping flag. A fixed certified evaluator interprets each description on an observation. Each active round tests the majority guard, optionally raises the threshold, and requests one new predictor.

The supplied learner is an explicit program with its own efficiency and correctness obligations. We truncate its output to the declared description bound on every execution, including failures. The analysis must therefore certify the truncated predictor. This gives a polynomial bound on the complete state throughout the clocked loop without a probabilistic runtime exception.

Main definitions

• State, Parameters: stored predictor descriptions and explicit resource parameters.
• round, run: the sampled body and its clocked iteration.

Main results

• round_bounded, run_bounded: every execution preserves the storage invariant.
• isPPTOn_round, isPPTOn_run: compositional certificates for the complete programs.

References

[Hol05], Section 2.2, Figure 2 and Lemma 2.14. The proved polynomial clock replaces the worst-dense-set stopping test. The majority test remains explicit and uses finite fair-bit sampling. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

structure Cslib.Crypto.Pseudoentropy.Boosting.State : Type

The executable state of the boosting loop. Predictor descriptions are ordinary binary words.

• stopped : Bool

  Once true, all remaining clock ticks preserve this state.

• threshold : ℕ

  The number of shifts subtracted from the raw vote margin.

• predictors : List (List Bool)

  Predictor descriptions, newest first.

def Cslib.Crypto.Pseudoentropy.Boosting.instDecidableEqState.decEq (x✝ x✝¹ : State) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Crypto.Pseudoentropy.Boosting.instDecidableEqState : DecidableEq State

def Cslib.Crypto.Pseudoentropy.Boosting.State.encoding : State ↪ List Bool

Reuse the standard Boolean, unary, and list encodings.

def Cslib.Crypto.Pseudoentropy.Boosting.State.initial : State

Start before any learned predictors or threshold shifts.

def Cslib.Crypto.Pseudoentropy.Boosting.State.votes (evaluate : List Bool → List Bool → Bool) (state : State) (observation : List Bool) : List Bool

Evaluate the current collection on an observation. The truth label is not an input.

def Cslib.Crypto.Pseudoentropy.Boosting.State.shift (state : State) (yes : Bool) : State

Move the threshold according to the sampled shift decision.

def Cslib.Crypto.Pseudoentropy.Boosting.State.add (state : State) (bound : ℕ) (code : List Bool) : State

Add a bounded predictor description.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.votes_initial (evaluate : List Bool → List Bool → Bool) (observation : List Bool) : votes evaluate initial observation = []

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.votes_shift (evaluate : List Bool → List Bool → Bool) (state : State) (yes : Bool) (observation : List Bool) : votes evaluate (state.shift yes) observation = votes evaluate state observation

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.votes_add (evaluate : List Bool → List Bool → Bool) (state : State) (bound : ℕ) (code observation : List Bool) : votes evaluate (state.add bound code) observation = evaluate (List.take bound code) observation :: votes evaluate state observation

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.length_encoding (state : State) : (encoding state).length = 2 * state.threshold + ((Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits) state.predictors).length + 4

def Cslib.Crypto.Pseudoentropy.Boosting.State.Bounded (rounds codeBound : ℕ) (state : State) : Prop

After rounds rounds there are at most that many shifts and bounded descriptions.

@[simp]

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.bounded_initial (codeBound : ℕ) : Bounded 0 codeBound initial

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.Bounded.mono {rounds more codeBound : ℕ} {state : State} (h : Bounded rounds codeBound state) (hmore : rounds ≤ more) : Bounded more codeBound state

A bound remains valid when more rounds are allowed.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.Bounded.shift_add {rounds codeBound : ℕ} {state : State} (h : Bounded rounds codeBound state) (yes : Bool) (code : List Bool) : Bounded (rounds + 1) codeBound ((state.shift yes).add codeBound code)

An optional shift and a truncated description preserve the resource invariant.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.Bounded.length_encoding_le {rounds codeBound : ℕ} {state : State} (h : Bounded rounds codeBound state) : (encoding state).length ≤ rounds * (2 * codeBound + 3) + 4

The semantic resource invariant bounds the complete encoded state.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.isPolyTime_mk {α : Type} {input : α ↪ List Bool} {stopped : α → Bool} {threshold : α → ℕ} {predictors : α → List (List Bool)} (hstopped : Turing.MultiTapeTM.ComputableTidilyInPolyTime stopped input Turing.MultiTapeTM.encBool) (hthreshold : Turing.MultiTapeTM.ComputableTidilyInPolyTime threshold input Turing.MultiTapeTM.encUnary) (hpredictors : Turing.MultiTapeTM.ComputableTidilyInPolyTime predictors input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => { stopped := stopped a, threshold := threshold a, predictors := predictors a }) input encoding

Efficient field values construct an efficient state.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.isPolyTime_stopped {α : Type} {input : α ↪ List Bool} {state : α → State} (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (state a).stopped) input Turing.MultiTapeTM.encBool

Project the stopping flag through the shared pair implementation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.isPolyTime_threshold {α : Type} {input : α ↪ List Bool} {state : α → State} (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (state a).threshold) input Turing.MultiTapeTM.encUnary

Project the threshold through the shared pair implementation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.isPolyTime_predictors {α : Type} {input : α ↪ List Bool} {state : α → State} (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (state a).predictors) input (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBits)

Project the predictor collection through the shared pair implementation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.isPolyTime_votes {α : Type} {input : α ↪ List Bool} {state : α → State} {evaluate : List Bool → List Bool → Bool} {observation : α → List Bool} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input encoding) (hobservation : Turing.MultiTapeTM.ComputableTidilyInPolyTime observation input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => votes evaluate (state a) (observation a)) input Turing.MultiTapeTM.encBits

Evaluating a list of descriptions is an ordinary captured map.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.isPolyTime_shift {α : Type} {input : α ↪ List Bool} {state : α → State} {yes : α → Bool} (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input encoding) (hyes : Turing.MultiTapeTM.ComputableTidilyInPolyTime yes input Turing.MultiTapeTM.encBool) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (state a).shift (yes a)) input encoding

Updating the threshold uses its field certificate and the efficient Boolean decision.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.isPolyTime_add {α : Type} {input : α ↪ List Bool} {state : α → State} {bound : α → ℕ} {code : α → List Bool} (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input encoding) (hbound : Turing.MultiTapeTM.ComputableTidilyInPolyTime bound input Turing.MultiTapeTM.encUnary) (hcode : Turing.MultiTapeTM.ComputableTidilyInPolyTime code input Turing.MultiTapeTM.encBits) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (state a).add (bound a) (code a)) input encoding

Truncation and list insertion charge for the complete stored predictor description.

structure Cslib.Crypto.Pseudoentropy.Boosting.Parameters : Type

Natural parameters for exact dyadic weights and polynomial sampling budgets.

• confidence : ℕ

  Each sampled guard has failure probability at most 2⁻confidence.

• densityNumerator : ℕ

  The numerator of the target density.

• densityBound : ℕ

  The parameter whose dyadicSize is the density denominator.

• rateBound : ℕ

  The parameter whose dyadicSize is the reciprocal weight rate.

• codeBound : ℕ

  Maximum length of each stored predictor description.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.encoding : Parameters ↪ List Bool

Store all five resource parameters in unary using the shared product encoding.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_mk {α : Type} {input : α ↪ List Bool} {confidence densityNumerator densityBound rateBound codeBound : α → ℕ} (hconfidence : Turing.MultiTapeTM.ComputableTidilyInPolyTime confidence input Turing.MultiTapeTM.encUnary) (hdensityNumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityNumerator input Turing.MultiTapeTM.encUnary) (hdensityBound : Turing.MultiTapeTM.ComputableTidilyInPolyTime densityBound input Turing.MultiTapeTM.encUnary) (hrateBound : Turing.MultiTapeTM.ComputableTidilyInPolyTime rateBound input Turing.MultiTapeTM.encUnary) (hcodeBound : Turing.MultiTapeTM.ComputableTidilyInPolyTime codeBound input Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => { confidence := confidence a, densityNumerator := densityNumerator a, densityBound := densityBound a, rateBound := rateBound a, codeBound := codeBound a }) input encoding

Computing the five fields suffices to construct the encoded parameter record.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_confidence {α : Type} {input : α ↪ List Bool} {params : α → Parameters} (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (params a).confidence) input Turing.MultiTapeTM.encUnary

Project the confidence through the shared product implementation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_densityNumerator {α : Type} {input : α ↪ List Bool} {params : α → Parameters} (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (params a).densityNumerator) input Turing.MultiTapeTM.encUnary

Project the density numerator through the shared product implementation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_densityBound {α : Type} {input : α ↪ List Bool} {params : α → Parameters} (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (params a).densityBound) input Turing.MultiTapeTM.encUnary

Project the density parameter through the shared product implementation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_rateBound {α : Type} {input : α ↪ List Bool} {params : α → Parameters} (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (params a).rateBound) input Turing.MultiTapeTM.encUnary

Project the rate parameter through the shared product implementation.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_codeBound {α : Type} {input : α ↪ List Bool} {params : α → Parameters} (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (params a).codeBound) input Turing.MultiTapeTM.encUnary

Project the description bound through the shared product implementation.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.denominator (params : Parameters) : ℕ

The density denominator is a positive power of two.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.inverseRate (params : Parameters) : ℕ

The reciprocal weight rate is a positive power of two.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.majorityPrecision (params : Parameters) : ℕ

A sufficient majority-test precision for every positive density numerator.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.shiftPrecision (params : Parameters) : ℕ

A sufficient density-test precision at weight rate 1 / inverseRate.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.clock (params : Parameters) : ℕ

A polynomial clock whenever 0 < densityNumerator ≤ denominator.

def Cslib.Crypto.Pseudoentropy.Boosting.withVotes (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (state : State) : ProbComp (List Bool × Bool)

Draw a fresh labeled observation and evaluate the current predictor collection on it.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_withVotes {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {source : α → ProbComp (List Bool × Bool)} {state : α → State} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hstate : Turing.MultiTapeTM.ComputableTidilyInPolyTime state input State.encoding) : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) fun (a : α) => withVotes evaluate (source a) (state a)

Training samples compose with the certified evaluator without exposing a machine.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.round (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (learn : State → ProbComp (List Bool)) (params : Parameters) (state : State) : ProbComp State

One round of boosting. A previously stopped state is returned unchanged.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.run (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (learn : State → ProbComp (List Bool)) (params : Parameters) : ProbComp State

Run the sampled boosting body for the proved polynomial clock.

theorem Cslib.Crypto.Pseudoentropy.Boosting.round_bounded (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (learn : State → ProbComp (List Bool)) (params : Parameters) {rounds : ℕ} {state : State} (hstate : State.Bounded rounds params.codeBound state) (next : State) : next ∈ (round evaluate source learn params state).eval.support → State.Bounded (rounds + 1) params.codeBound next

Resource bounds hold on every outcome, including erroneous tests and learner failures.

theorem Cslib.Crypto.Pseudoentropy.Boosting.run_bounded (evaluate : List Bool → List Bool → Bool) (source : ProbComp (List Bool × Bool)) (learn : State → ProbComp (List Bool)) (params : Parameters) (state : State) : state ∈ (run evaluate source learn params).eval.support → State.Bounded params.clock params.codeBound state

The clocked loop stores at most one bounded predictor per round.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_round {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {source : α → ProbComp (List Bool × Bool)} {learn : α → State → ProbComp (List Bool)} {params : α → Parameters} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hlearn : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input State.encoding) Turing.MultiTapeTM.encBits fun (pair : α × State) => learn pair.1 pair.2) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Parameters.encoding) : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input State.encoding) State.encoding fun (pair : α × State) => round evaluate (source pair.1) (learn pair.1) (params pair.1) pair.2

The complete sampled round composes the evaluator, source, learner, and unary parameters. No machine implementation is part of the client's proof.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_run {α : Type} {input : α ↪ List Bool} {evaluate : List Bool → List Bool → Bool} {source : α → ProbComp (List Bool × Bool)} {learn : α → State → ProbComp (List Bool)} {params : α → Parameters} (hevaluate : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (pair : List Bool × List Bool) => evaluate pair.1 pair.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) (hlearn : Probability.IsPPTOn (Turing.MultiTapeTM.encPair input State.encoding) Turing.MultiTapeTM.encBits fun (pair : α × State) => learn pair.1 pair.2) (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input Parameters.encoding) : Probability.IsPPTOn input State.encoding fun (a : α) => run evaluate (source a) (learn a) (params a)

Polynomially bounded parameters and a certified learner give a strict PPT boosting loop. The single resource invariant also proves run_bounded, independently of correctness.