Checking that a witness is consistent

A witness records an answer for every query slot. It comes from an actual proof only if slots reading the same proof position carry the same answer, and that is what this module checks: four nested loops over a pair of coin strings and a pair of query indices.

The check never looks at a position as a number. posAt returns each query position as its own serialization, so slots reading the same position are recognised by comparing strings — and a slot past the end of a query list is recognised by that string being empty.

Main definitions

• Complexity.consLang — the consistency check, as a language of pair x w

Main results

• Complexity.consLang_mem_P — the check is polynomial time

Reading the nested loop input

The innermost input is pair (pair (pair (pair (pair x w) ρ) ρ') i) i', with the four loop indices in unary.

def Complexity.conY2 (y : List Bool) : List Bool

Strip the last two indices.

Equations

• Complexity.conY2 y = Complexity.pairFst (Complexity.pairFst y)

def Complexity.conY1 (y : List Bool) : List Bool

Strip the last three indices.

Equations

• Complexity.conY1 y = Complexity.pairFst (Complexity.conY2 y)

def Complexity.conY0 (y : List Bool) : List Bool

The original pair x w.

Equations

• Complexity.conY0 y = Complexity.pairFst (Complexity.conY1 y)

def Complexity.conX (y : List Bool) : List Bool

The input.

Equations

• Complexity.conX y = Complexity.pairFst (Complexity.conY0 y)

def Complexity.conW (y : List Bool) : List Bool

The witness.

Equations

• Complexity.conW y = Complexity.pairSnd (Complexity.conY0 y)

def Complexity.conC1 (y : List Bool) : ℕ

The first coin index.

Equations

• Complexity.conC1 y = (Complexity.pairSnd (Complexity.conY1 y)).length

def Complexity.conC2 (y : List Bool) : ℕ

The second coin index.

Equations

• Complexity.conC2 y = (Complexity.pairSnd (Complexity.conY2 y)).length

def Complexity.conC3 (y : List Bool) : ℕ

The first query index.

Equations

• Complexity.conC3 y = (Complexity.pairSnd (Complexity.pairFst y)).length

def Complexity.conC4 (y : List Bool) : ℕ

The second query index.

Equations

• Complexity.conC4 y = (Complexity.pairSnd y).length

theorem Complexity.conY2_mem_FP : conY2 ∈ FP

theorem Complexity.conY1_mem_FP : conY1 ∈ FP

theorem Complexity.conY0_mem_FP : conY0 ∈ FP

theorem Complexity.conX_mem_FP : conX ∈ FP

theorem Complexity.conW_mem_FP : conW ∈ FP

theorem Complexity.unary_conC1_mem_FP : (fun (y : List Bool) => List.replicate (conC1 y) true) ∈ FP

theorem Complexity.unary_conC2_mem_FP : (fun (y : List Bool) => List.replicate (conC2 y) true) ∈ FP

theorem Complexity.unary_conC3_mem_FP : (fun (y : List Bool) => List.replicate (conC3 y) true) ∈ FP

theorem Complexity.unary_conC4_mem_FP : (fun (y : List Bool) => List.replicate (conC4 y) true) ∈ FP

The check

noncomputable def Complexity.conRho (r : ℕ → ℕ) (y : List Bool) : List Bool

The first coin string.

Equations

• Complexity.conRho r y = Complexity.coinStr (r (Complexity.conX y).length) (Complexity.conC1 y)

noncomputable def Complexity.conRho' (r : ℕ → ℕ) (y : List Bool) : List Bool

The second coin string.

Equations

• Complexity.conRho' r y = Complexity.coinStr (r (Complexity.conX y).length) (Complexity.conC2 y)

noncomputable def Complexity.conP (f : List Bool → List Bool) (r : ℕ → ℕ) (y : List Bool) : List Bool

The position the first slot queries, as a string.

Equations

• Complexity.conP f r y = Complexity.posAt (f (Complexity.pair (Complexity.conX y) (Complexity.conRho r y))) (Complexity.conC3 y)

noncomputable def Complexity.conP' (f : List Bool → List Bool) (r : ℕ → ℕ) (y : List Bool) : List Bool

The position the second slot queries, as a string.

Equations

• Complexity.conP' f r y = Complexity.posAt (f (Complexity.pair (Complexity.conX y) (Complexity.conRho' r y))) (Complexity.conC4 y)

def Complexity.conB (Q : ℕ) (y : List Bool) : List Bool

The answer recorded in the first slot.

Equations

• Complexity.conB Q y = Complexity.wBlock (Complexity.conW y) (Complexity.conC1 y * Q + Complexity.conC3 y) 1

def Complexity.conB' (Q : ℕ) (y : List Bool) : List Bool

The answer recorded in the second slot.

Equations

• Complexity.conB' Q y = Complexity.wBlock (Complexity.conW y) (Complexity.conC2 y * Q + Complexity.conC4 y) 1

noncomputable def Complexity.conChk (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (y : List Bool) : List Bool

The verdict of one iteration: when both slots are real and query the same position, their answers must agree.

Equations

• One or more equations did not get rendered due to their size.

Polynomial time

theorem Complexity.conRho_mem_FP (r : ℕ → ℕ) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : conRho r ∈ FP

theorem Complexity.conRho'_mem_FP (r : ℕ → ℕ) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : conRho' r ∈ FP

theorem Complexity.conP_mem_FP (f : List Bool → List Bool) (r : ℕ → ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : conP f r ∈ FP

theorem Complexity.conP'_mem_FP (f : List Bool → List Bool) (r : ℕ → ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : conP' f r ∈ FP

theorem Complexity.offset_mem_FP (Q : ℕ) {c d : List Bool → ℕ} (hc : (fun (y : List Bool) => List.replicate (c y) true) ∈ FP) (hd : (fun (y : List Bool) => List.replicate (d y) true) ∈ FP) : (fun (y : List Bool) => List.replicate (c y * Q + d y) false) ∈ FP

The offset of a slot in the witness, in unary.

theorem Complexity.conB_mem_FP (Q : ℕ) : conB Q ∈ FP

theorem Complexity.conB'_mem_FP (Q : ℕ) : conB' Q ∈ FP

theorem Complexity.conChk_mem_FP (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : conChk f r Q ∈ FP

noncomputable def Complexity.consInner (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) : Language

One iteration of the consistency check.

Equations

• Complexity.consInner f r Q = {y : List Bool | ∃ b ∈ Complexity.conChk f r Q y, b = true}

theorem Complexity.consInner_mem_P (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) : consInner f r Q ∈ P

noncomputable def Complexity.consL3 (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) : Language

The two inner loops, over the pair of query indices.

Equations

• Complexity.consL3 f r Q = {y : List Bool | ∀ i' < Q, Complexity.pair y (List.replicate i' true) ∈ Complexity.consInner f r Q}

noncomputable def Complexity.consL2 (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) : Language

The outer of the two query-index loops.

Equations

• Complexity.consL2 f r Q = {y : List Bool | ∀ i < Q, Complexity.pair y (List.replicate i true) ∈ Complexity.consL3 f r Q}

noncomputable def Complexity.consL1 (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) : Language

The outer loop over the second coin string.

Equations

• Complexity.consL1 f r Q = {y : List Bool | ∀ c' < 2 ^ r (Complexity.pairFst (Complexity.pairFst y)).length, Complexity.pair y (List.replicate c' true) ∈ Complexity.consL2 f r Q}

noncomputable def Complexity.consLang (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) : Language

The consistency check, as a language of pair x w.

Equations

• Complexity.consLang f r Q = {z : List Bool | ∀ c < 2 ^ r (Complexity.pairFst z).length, Complexity.pair z (List.replicate c true) ∈ Complexity.consL1 f r Q}

theorem Complexity.consLang_mem_P (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hf : f ∈ FP) (hr : (fun (x : List Bool) => List.replicate (r x.length) true) ∈ FP) (hrlog : BigO r fun (n : ℕ) => Nat.log 2 n) : consLang f r Q ∈ P

What one iteration says

theorem Complexity.exists_eqFlag_iff (a b : List Bool) : (∃ z ∈ Cobham.eqFlag a b, z = true) ↔ a = b

theorem Complexity.mem_consInner_iff (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (y : List Bool) : y ∈ consInner f r Q ↔ conP f r y = conP' f r y ∧ conP f r y ≠ [] → conB Q y = conB' Q y

def Complexity.conArg (x w : List Bool) (c c' i i' : ℕ) : List Bool

The packed input of one iteration.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.conX_arg (x w : List Bool) (c c' i i' : ℕ) : conX (conArg x w c c' i i') = x

@[simp]

theorem Complexity.conW_arg (x w : List Bool) (c c' i i' : ℕ) : conW (conArg x w c c' i i') = w

@[simp]

theorem Complexity.conC1_arg (x w : List Bool) (c c' i i' : ℕ) : conC1 (conArg x w c c' i i') = c

@[simp]

theorem Complexity.conC2_arg (x w : List Bool) (c c' i i' : ℕ) : conC2 (conArg x w c c' i i') = c'

@[simp]

theorem Complexity.conC3_arg (x w : List Bool) (c c' i i' : ℕ) : conC3 (conArg x w c c' i i') = i

@[simp]

theorem Complexity.conC4_arg (x w : List Bool) (c c' i i' : ℕ) : conC4 (conArg x w c c' i i') = i'

The pieces on a packed argument

theorem Complexity.conRho_arg (r : ℕ → ℕ) {x w : List Bool} {c c' i i' : ℕ} (hc : c < 2 ^ r x.length) : conRho r (conArg x w c c' i i') = BitString.toList (PCPVerifier.coinOfIndex ⟨c, hc⟩)

theorem Complexity.conRho'_arg (r : ℕ → ℕ) {x w : List Bool} {c c' i i' : ℕ} (hc' : c' < 2 ^ r x.length) : conRho' r (conArg x w c c' i i') = BitString.toList (PCPVerifier.coinOfIndex ⟨c', hc'⟩)

theorem Complexity.conP_arg (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) {x w : List Bool} {c c' i i' : ℕ} (hc : c < 2 ^ r x.length) : conP f r (conArg x w c c' i i') = posAt (DataEncode.bitstringEncode (V.positions x (BitString.toList (PCPVerifier.coinOfIndex ⟨c, hc⟩)))) i

theorem Complexity.conP'_arg (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) {x w : List Bool} {c c' i i' : ℕ} (hc' : c' < 2 ^ r x.length) : conP' f r (conArg x w c c' i i') = posAt (DataEncode.bitstringEncode (V.positions x (BitString.toList (PCPVerifier.coinOfIndex ⟨c', hc'⟩)))) i'

theorem Complexity.conB_arg (Q : ℕ) {x w : List Bool} {c c' i i' : ℕ} (hk : c * Q + i < w.length) : conB Q (conArg x w c c' i i') = [w.getD (c * Q + i) false]

theorem Complexity.conB'_arg (Q : ℕ) {x w : List Bool} {c c' i i' : ℕ} (hk : c' * Q + i' < w.length) : conB' Q (conArg x w c c' i i') = [w.getD (c' * Q + i') false]

Unfolding the loops

theorem Complexity.mem_consLang_iff_forall (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (x w : List Bool) : pair x w ∈ consLang f r Q ↔ ∀ c < 2 ^ r x.length, ∀ c' < 2 ^ r x.length, ∀ i < Q, ∀ i' < Q, conArg x w c c' i i' ∈ consInner f r Q

The check is consistency

theorem Complexity.mem_consLang_iff (V : PCPVerifier) (f : List Bool → List Bool) (r : ℕ → ℕ) (Q : ℕ) (hfspec : ∀ (x rr : List Bool), f (pair x rr) = DataEncode.bitstringEncode (V.positions x rr)) {x w : List Bool} (hw : w.length = 2 ^ r x.length * Q) (hQ : ∀ (rr : List Bool), (V.positions x rr).length ≤ Q) : pair x w ∈ consLang f r Q ↔ V.Consistent (r x.length) x (V.tableOf (r x.length) Q x w)

The consistency check says exactly what it should.