Reading a verifier's query list

A PCPVerifier hands over its query positions only as an encoded list — that is what positions_mem provides, and it is all a polynomial-time algorithm can have, since a single position may be astronomically large. This module reads individual entries back out of that encoding with the bracket scan.

Two facts make the reading enough for everything downstream. A position is recovered as its own serialization, so two positions can be compared by comparing strings, with no arithmetic on the values; and an index past the end of the list is recognisable, because every serialization is non-empty.

Main definitions

• Complexity.posInner — the encoding stripped of its outer brackets
• Complexity.posAt, Complexity.posCount — one entry, and how many there are

Main results

• Complexity.posAt_eq, Complexity.posCount_eq — what the scan reads
• Complexity.posAt_eq_iff — comparing entries compares positions

def Complexity.posInner (e : List Bool) : List Bool

The serialized entries of an encoded list, with the outer brackets removed: the string the scan consumes.

Equations

• Complexity.posInner e = List.take (e.length - 2) (List.drop 1 e)

theorem Complexity.posInner_mem_FP {a : List Bool → List Bool} (ha : a ∈ FP) : (fun (z : List Bool) => posInner (a z)) ∈ FP

noncomputable def Complexity.posAt (e : List Bool) (i : ℕ) : List Bool

The i-th entry of an encoded list, as its own serialization.

Equations

• Complexity.posAt e i = Complexity.DataScan.childOf Complexity.DataScan.scanPoly (Complexity.DataScan.scanArg i (Complexity.posInner e))

noncomputable def Complexity.posCount (e : List Bool) : List Bool

How many entries an encoded list has, in unary.

Equations

• Complexity.posCount e = Complexity.DataScan.childCount Complexity.DataScan.scanPoly (Complexity.DataScan.scanArg 0 (Complexity.posInner e))

theorem Complexity.posAt_mem_FP {a b : List Bool → List Bool} (ha : a ∈ FP) (hb : b ∈ FP) : (fun (z : List Bool) => posAt (b z) (a z).length) ∈ FP

theorem Complexity.posCount_mem_FP {b : List Bool → List Bool} (hb : b ∈ FP) : (fun (z : List Bool) => posCount (b z)) ∈ FP

What the scan reads

theorem Complexity.posInner_bitstringEncode {α : Type} [DataEncode α] (l : List α) : posInner (DataEncode.bitstringEncode l) = (List.map Data.toBits (List.map DataEncode.encode l)).flatten

theorem Complexity.posCount_eq {α : Type} [DataEncode α] (l : List α) : posCount (DataEncode.bitstringEncode l) = List.replicate l.length true

theorem Complexity.posAt_eq {α : Type} [DataEncode α] (l : List α) (i : ℕ) : posAt (DataEncode.bitstringEncode l) i = (Option.map Data.toBits (List.map DataEncode.encode l)[i]?).getD []

theorem Complexity.posAt_eq_of_lt {α : Type} [DataEncode α] {l : List α} {i : ℕ} (h : i < l.length) : posAt (DataEncode.bitstringEncode l) i = DataEncode.bitstringEncode l[i]

theorem Complexity.posAt_eq_nil {α : Type} [DataEncode α] {l : List α} {i : ℕ} (h : l.length ≤ i) : posAt (DataEncode.bitstringEncode l) i = []

theorem Complexity.posAt_ne_nil {α : Type} [DataEncode α] {l : List α} {i : ℕ} (h : i < l.length) : posAt (DataEncode.bitstringEncode l) i ≠ []

theorem Complexity.bitstringEncode_append {α : Type} [DataEncode α] (l₁ l₂ : List α) : DataEncode.bitstringEncode (l₁ ++ l₂) = false :: (posInner (DataEncode.bitstringEncode l₁) ++ posInner (DataEncode.bitstringEncode l₂)) ++ [true]

Concatenating encoded lists. The encoding of an append is the two inner parts, one after the other, inside a fresh pair of brackets.

theorem Complexity.posAt_eq_iff {α : Type} [DataEncode α] {l l' : List α} {i i' : ℕ} (h : i < l.length) (h' : i' < l'.length) : posAt (DataEncode.bitstringEncode l) i = posAt (DataEncode.bitstringEncode l') i' ↔ l[i] = l'[i']

Comparing entries compares positions. The scan returns each entry's own serialization, and that serialization determines the entry.