Sampling a random string and running a verifier, within explicit time

A fair-coin machine can draw a uniformly random string w of length ℓ a and output the verdict V (a, w) of a deterministic verifier on the pair (a, w), within the time it takes to write ℓ a in unary and to run the verifier, up to constant factors (Cslib.Complexity.exists_machine_sampleVerify_of_bound). The machine is a closed fair-coin composition:

• a deterministic machine writes frame (enc a) followed by ℓ a ones;
• the fixed sampler Turing.MultiTapePTM.pairSampler copies the framed instance and replaces the ones by fair coins;
• a deterministic machine runs the verifier.

Every run halts within the clock, and the output is distributed as [V (a, w)] for w uniform of length ℓ a. Read nondeterministically, the machine guesses and verifies a certificate (Cslib.Complexity.setOf_exists_mem_NTIME); read probabilistically, it samples and verifies (Cslib.Complexity.mem_PromiseBPTIME_of_verifier). Unlike the polynomial compiler of PPT programs (Cslib.Probability.IsPPTOn.exists_halting_machine), the clock keeps the time bound up to constant factors.

Main results

• Cslib.Complexity.exists_machine_sampleVerify_of_bound: the sample-and-verify machine within O(B a) steps for a per-instance bound B, with its output distribution.
• Cslib.Complexity.exists_machine_sampleVerify: the same within O(t n) steps on inputs of length n.

theorem Cslib.Complexity.exists_machine_sampleVerify_of_bound {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {ℓ Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {B : α → ℕ} (hℓ : Turing.MultiTapeTM.ComputableInO ℓ enc Turing.MultiTapeTM.encUnary Tℓ Sℓ) (hV : Turing.MultiTapeTM.ComputableInO V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool T S) (hB : ∀ (a : α) (w : List Bool), w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ B a) : ∃ (c : ℕ) (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapePTM k Bool State), ∀ (a : α), (∀ final ∈ (machine.runClosedConfigFrom (c * B a + c) (Turing.MultiTapeMachine.initialConfig machine (enc a))).eval.support, final.tapes.state = none) ∧ (machine.runClosed (c * B a + c) (enc a)).eval = PMF.map (fun (w : List Bool) => [V (a, w)]) (BitString.uniformList (ℓ a))

Sample and verify, within a per-instance bound. If a verifier V is computable within time T (a, w) on encoded pairs, the length ℓ a of the random string is computable in unary within time Tℓ a, and (enc a).length + Tℓ a + T (a, w) ≤ B a for every string w of length ℓ a, then a fair-coin machine with a binary alphabet and finitely many states halts on every run within time c * B a + c and outputs [V (a, w)] for a uniformly random w of length ℓ a.

theorem Cslib.Complexity.exists_machine_sampleVerify {α : Type} {enc : α ↪ List Bool} {V : α × List Bool → Bool} {ℓ : α → ℕ} {t : ℕ → ℕ} {Tℓ Sℓ : α → ℕ} {T S : α × List Bool → ℕ} {C : ℕ} (hℓ : Turing.MultiTapeTM.ComputableInO ℓ enc Turing.MultiTapeTM.encUnary Tℓ Sℓ) (hV : Turing.MultiTapeTM.ComputableInO V (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool T S) (ht : ∀ (a : α) (w : List Bool), w.length = ℓ a → (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C) : ∃ (c₁ : ℕ) (c₂ : ℕ) (k : ℕ) (State : Type) (_ : Finite State) (machine : Turing.MultiTapePTM k Bool State), ∀ (a : α), (∀ final ∈ (machine.runClosedConfigFrom (c₁ * t (enc a).length + c₂) (Turing.MultiTapeMachine.initialConfig machine (enc a))).eval.support, final.tapes.state = none) ∧ (machine.runClosed (c₁ * t (enc a).length + c₂) (enc a)).eval = PMF.map (fun (w : List Bool) => [V (a, w)]) (BitString.uniformList (ℓ a))

Sample and verify, within explicit time. If a verifier V is computable within time T (a, w) on encoded pairs, and the length ℓ a of the random string is computable in unary within time Tℓ a, and (enc a).length + Tℓ a + T (a, w) ≤ C * t (enc a).length + C for every string w of length ℓ a, then a fair-coin machine with a binary alphabet and finitely many states halts on every run within time c₁ * t (enc a).length + c₂ and outputs [V (a, w)] for a uniformly random w of length ℓ a.