Running a verifier on a sampled certificate

The program that samples a uniform word of length p evaluated at the encoded input length and returns the verdict of a Boolean verifier V on the input and that word. This is the common first step from verifier classes (NP, BPP, PP) to fair-coin machines: the program is uniformly PPT, and the encoded output [true] is possible exactly when some word of the sampled length is accepted.

Main results

• Cslib.Probability.isPPTOn_sampleVerify: a polynomial-time verifier run on a sampled word of polynomial length is uniformly strict PPT.
• Cslib.Probability.singleton_true_mem_support_sampleVerify_iff: the encoded verdict [true] is possible exactly when some word of the sampled length is accepted.

theorem Cslib.Probability.isPPTOn_sampleVerify {α : Type} {enc : α ↪ List Bool} (p : Polynomial ℕ) {V : α × List Bool → Bool} (hV : Turing.MultiTapeTM.ComputableInPolyTime V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool) : IsPPTOn enc Turing.MultiTapeTM.encBool fun (a : α) => (fun (w : List Bool) => V (a, w)) <$> BitString.sampleList (Polynomial.eval (enc a).length p)

A polynomial-time verifier run on a uniformly sampled word whose length is a fixed polynomial in the encoded input length is a uniform strict PPT program.

theorem Cslib.Probability.singleton_true_mem_support_sampleVerify_iff {α : Type} (V : α × List Bool → Bool) (a : α) (n : ℕ) : [true] ∈ (PMF.map (⇑Turing.MultiTapeTM.encBool) ((fun (w : List Bool) => V (a, w)) <$> BitString.sampleList n).eval).support ↔ ∃ (w : List Bool), w.length = n ∧ V (a, w) = true

Running V on a uniform word of length n can output the encoded verdict [true] exactly when some word of length n is accepted.