Strict PPT empirical selection

Candidate selection composes an efficient indexed trial with polynomial candidate and repetition counts. The common adaptive-loop certificate charges for both indices and the running success count. Their bounds hold on every execution, independently of the statistical accuracy theorem.

Main results

• Cslib.Probability.IsPPTOn.selectBest: certify a complete indexed search.
• Cslib.Probability.IsPPTOn.selectFrom: charge the input list, lookup and validation.
• Cslib.Probability.IsPPTOn.sampleBest: compose candidate generation and selection.

References

Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Probability.IsPPTOn.selectBest {α : Type} {input : α ↪ List Bool} {count trials : α → ℕ} {test : α → ℕ → ProbComp Bool} (htest : IsPPTOn (Turing.MultiTapeTM.encPair input Turing.MultiTapeTM.encUnary) Turing.MultiTapeTM.encBool fun (pair : α × ℕ) => test pair.1 pair.2) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (htrials : Turing.MultiTapeTM.ComputableTidilyInPolyTime trials input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encUnary fun (a : α) => OracleComp.selectBest (count a) (trials a) (test a)

Selecting among polynomially many efficient tests using polynomially many trials is strict PPT. The test may capture the complete original input.

theorem Cslib.Probability.IsPPTOn.selectFrom {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {values : α → List β} {trials : α → ℕ} {test : α → β → ProbComp Bool} (fallback : β) (hvalues : Turing.MultiTapeTM.ComputableTidilyInPolyTime values input (Turing.MultiTapeTM.encList output)) (htrials : Turing.MultiTapeTM.ComputableTidilyInPolyTime trials input Turing.MultiTapeTM.encUnary) (htest : IsPPTOn (Turing.MultiTapeTM.encPair input output) Turing.MultiTapeTM.encBool fun (pair : α × β) => test pair.1 pair.2) : IsPPTOn input output fun (a : α) => OracleComp.selectFrom (values a) (trials a) (test a) fallback

Selecting from an efficiently computed list charges for the whole list and each test.

theorem Cslib.Probability.IsPPTOn.sampleBest {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {source : α → ProbComp β} {test : α → β → ProbComp Bool} {count trials : α → ℕ} (fallback : β) (hsource : IsPPTOn input output source) (htest : IsPPTOn (Turing.MultiTapeTM.encPair input output) Turing.MultiTapeTM.encBool fun (pair : α × β) => test pair.1 pair.2) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (htrials : Turing.MultiTapeTM.ComputableTidilyInPolyTime trials input Turing.MultiTapeTM.encUnary) : IsPPTOn input output fun (a : α) => OracleComp.sampleBest (count a) (trials a) (source a) (test a) fallback

Sampling a polynomial candidate pool and selecting empirically is a uniform strict PPT program. Both the generator and the validation test may capture the original input.