The walk runs on the protocol's tree

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.IPSem builds a machine that walks an abstract tree, parametric in a single test — does this coin string make the verifier accept below these rounds. This file supplies that test from a protocol and checks that the tree the machine walks is the protocol's own.

Main definitions

• Complexity.Protocol.walkParams — the parameters the walk runs on

Main results

• Complexity.Protocol.treeVal_eq_gvalR — the abstract tree is the protocol's game tree
• Complexity.Protocol.treeVal_le_two_pow — its values fit in the coin space
• Complexity.Protocol.ipStep_iterate_walk — the encoded orbit is the abstract one

noncomputable def Complexity.Protocol.walkParams (prot : Protocol) (x : List Bool) : IPM.Params

The parameters the walk runs on: the message bound, the coin width, and the leaf test.

Equations

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

theorem Complexity.Protocol.treeVal_eq_gvalR (prot : Protocol) (x : List Bool) (n : ℕ) (ps : List (List Bool × List Bool)) : IPM.treeVal (prot.walkParams x) n ps = prot.gvalR x (prot.coins x.length) n ps

The abstract tree is the protocol's game tree.

theorem Complexity.Protocol.treeVal_le_two_pow (prot : Protocol) (x : List Bool) (n : ℕ) (ps : List (List Bool × List Bool)) : IPM.treeVal (prot.walkParams x) n ps ≤ 2 ^ (prot.walkParams x).t

The walk decides membership

theorem Complexity.Protocol.cmpBit_eq_true_iff {L : Language} (prot : Protocol) (x : List Bool) (hcomp : ∀ y ∈ L, ∃ (S : ProverStrategy), S.Bounded (prot.msgLen y.length) ∧ 2 / 3 ≤ eventProb (prot.acceptEvent S y)) (hsound : ∀ y ∉ L, ∀ (S : ProverStrategy), S.Bounded (prot.msgLen y.length) → eventProb (prot.acceptEvent S y) ≤ 1 / 3) (w : List Bool) (hwlen : w.length = (prot.walkParams x).t + 1) (hwval : binValLE w = IPM.treeVal (prot.walkParams x) (prot.rounds x.length) []) : IPM.cmpBit (prot.walkParams x) w = true ↔ x ∈ L

The verdict the walk finishes with is membership.

theorem Complexity.Protocol.walk_decides {L : Language} (prot : Protocol) (hcomp : ∀ y ∈ L, ∃ (S : ProverStrategy), S.Bounded (prot.msgLen y.length) ∧ 2 / 3 ≤ eventProb (prot.acceptEvent S y)) (hsound : ∀ y ∉ L, ∀ (S : ProverStrategy), S.Bounded (prot.msgLen y.length) → eventProb (prot.acceptEvent S y) ≤ 1 / 3) (x lvl : List Bool) (hlvl : lvl.length = prot.rounds x.length) : ∃ T ≤ IPM.runBound (prot.walkParams x) (prot.rounds x.length), (∀ j ≤ T, ((IPM.step (prot.walkParams x))^[j] { done := false, ansBit := false, ret := none, stk := [IPM.freshFrm (prot.walkParams x) [] lvl] }).done = false) ∧ ((IPM.step (prot.walkParams x))^[T + 1] { done := false, ansBit := false, ret := none, stk := [IPM.freshFrm (prot.walkParams x) [] lvl] }).done = true ∧ (((IPM.step (prot.walkParams x))^[T + 2] { done := false, ansBit := false, ret := none, stk := [IPM.freshFrm (prot.walkParams x) [] lvl] }).done = true ↔ x ∈ L)

The walk decides membership. From a single fresh frame of rounds(|x|) levels the machine keeps its flag down, raises it on the next step, and one step later the flag is the membership bit.

theorem Complexity.Protocol.ipStep_iterate_walk (prot : Protocol) (x mr cr : List Bool) (hm : mr.length = (prot.walkParams x).m) (hc : cr.length = (prot.walkParams x).t) (okf : List Bool → List Bool → List Bool) (lvl : List Bool) (hokf : ∀ (f : IPM.Frm) (fs : List IPM.Frm), IPM.BodyOk (f :: fs) → (f :: fs).length ≤ lvl.length + 1 → ∀ (u : List Bool), okf (IPM.encStk (f :: fs)) u = [(prot.walkParams x).ok (IPM.roundsOf fs) u]) (j : ℕ) : (IPM.ipStep mr cr okf)^[j] (IPM.encSst { done := false, ansBit := false, ret := none, stk := [IPM.freshFrm (prot.walkParams x) [] lvl] }) = IPM.encSst ((IPM.step (prot.walkParams x))^[j] { done := false, ansBit := false, ret := none, stk := [IPM.freshFrm (prot.walkParams x) [] lvl] })

The encoded orbit is the abstract one.