A verifier's query list from its positions

PCPVerifier asks for the query list in DataEncode form, which is not how an algorithm naturally describes it: an algorithm says "the i-th position is this number". This module bridges the two, so that building a verifier needs only a polynomial-time rule for each position, given in unary.

The width a number needs is the number itself — every v is below 2 ^ v — so no logarithms are involved: the same unary value serves as both the value and the width bound for natEncodeFn.

Main results

• Complexity.positions_mem_of_unary — a unary position rule gives positions_mem

theorem Complexity.fstBlock_length_le (z : List Bool) : (pairFst z).length ≤ z.length

noncomputable def Complexity.posEntryFn (P : List Bool → List Bool) (w : List Bool) : List Bool

The encoding of one position, read off a packed argument.

Equations

• Complexity.posEntryFn P w = Complexity.natEncodeFn (Complexity.pair (P w) (P w))

theorem Complexity.posEntryFn_mem_FP {P : List Bool → List Bool} (hP : P ∈ FP) : posEntryFn P ∈ FP

theorem Complexity.posEntryFn_eq {P : List Bool → List Bool} (w : List Bool) : posEntryFn P w = DataEncode.bitstringEncode (P w).length

theorem Complexity.positions_mem_of_unary {pos : List Bool → ℕ → ℕ} {cnt : List Bool → ℕ} (hcnt : (fun (z : List Bool) => List.replicate (cnt z) true) ∈ FP) {P : List Bool → List Bool} (hP : P ∈ FP) (hPspec : ∀ (z : List Bool) (i : ℕ), P (pair z (List.replicate i true)) = List.replicate (pos z i) true) : ∃ g ∈ FP, ∀ (z : List Bool), g z = DataEncode.bitstringEncode (List.map (pos z) (List.range (cnt z)))

A unary position rule gives the query list. If the number of queries and each query position are polynomial-time computable in unary, then the encoded query list is polynomial-time computable.