The walk of an interactive protocol's game tree

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.IPGameTree reduces membership in a language of IP to a recursion written as two counter loops:

gvalR 0       ps = #{coin strings that make the verifier accept below `ps`}
gvalR (n + 1) ps = ∑ over the verifier's messages, of the maximum over the prover's replies

This file is the machine that walks it, on an inductive state — the same discipline Savitch's theorem uses in Complexitylib.Classes.Containments.Internal.SavitchSem. A stack holds one frame per round, carrying the two message counters and the running sum and maximum; the bottom frame is a leaf, carrying the coin counter and its tally.

Everything the walk needs from the protocol is packed into Complexity.IPM.Params: the message bound, the coin width, and the single test does this coin string make the verifier accept, below these rounds.

Main definitions

• Complexity.IPM.Frm, Complexity.IPM.Sst — a frame and the machine's state
• Complexity.IPM.roundsOf — the rounds a stack records
• Complexity.IPM.step — one step of the walk

Main results

• the step_* lemmas — one for each shape the step can take

The data the walk needs

structure Complexity.IPM.Params : Type

What the walk needs to know about the protocol.

• m : ℕ

  The bound on either side's message length.

• t : ℕ

  The number of coins, so the width of a coin string.

• ok : List (List Bool × List Bool) → List Bool → Bool

  Does this coin string make the verifier accept, below these rounds?

def Complexity.IPM.zeroCount (P : Params) : List Bool

The zero of the width a count is held in: one bit more than the coin width, so that a count of up to 2 ^ t fits.

Equations

• Complexity.IPM.zeroCount P = List.replicate (P.t + 1) false

def Complexity.IPM.zeroCoin (P : Params) : List Bool

The first coin string.

Equations

• Complexity.IPM.zeroCoin P = List.replicate P.t false

The state

structure Complexity.IPM.Frm : Type

A frame of the walk: the rounds still to play, the two message counters, and the running sum and maximum. At a leaf a is the coin string and sum its tally.

• lvl : List Bool

  The rounds still to play, in unary.

• v : List Bool

  The verifier message currently being summed over.

• a : List Bool

  The prover reply currently being maximized over; the coin string at a leaf.

• sum : List Bool

  The running sum; the running tally at a leaf.

• best : List Bool

  The running maximum; unused at a leaf.

• body : List Bool

  The body of the encoding of the rounds below this frame. Carrying it is what makes the leaf's consistency test a per-frame check rather than a walk back down the stack.

structure Complexity.IPM.Sst : Type

The machine's state.

• done : Bool

  The bit the space-bounded iteration watches.

• ansBit : Bool

  The answer, once it is known.

• ret : Option (List Bool)

  The value a finished subtree is returning.

• stk : List Frm

  The stack, top frame first.

def Complexity.IPM.roundsOf (fs : List Frm) : List (List Bool × List Bool)

The rounds a stack records: the message pair of every frame below the top, in the order they were played.

Equations

• Complexity.IPM.roundsOf fs = (List.map (fun (g : Complexity.IPM.Frm) => (g.v, g.a)) fs).reverse

@[simp]

theorem Complexity.IPM.roundsOf_nil : roundsOf [] = []

@[simp]

theorem Complexity.IPM.roundsOf_cons (g : Frm) (fs : List Frm) : roundsOf (g :: fs) = roundsOf fs ++ [(g.v, g.a)]

@[simp]

theorem Complexity.IPM.roundsOf_length (fs : List Frm) : (roundsOf fs).length = fs.length

def Complexity.IPM.freshFrm (P : Params) (body lvl : List Bool) : Frm

The frame a node starts from: both counters at the first message, both accumulators zero, and the body of the rounds above it. At a leaf the coin counter starts at the first coin string instead.

Equations

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

def Complexity.IPM.childFrm (P : Params) (f : Frm) : Frm

The frame a branch pushes: a fresh node for the pair it is currently trying, carrying the body of the transcript that leads to it.

Equations

• Complexity.IPM.childFrm P f = Complexity.IPM.freshFrm P (f.body ++ Complexity.encMsg f.v ++ Complexity.encMsg f.a) (List.drop 1 f.lvl)

@[simp]

theorem Complexity.IPM.childFrm_lvl (P : Params) (f : Frm) : (childFrm P f).lvl = List.drop 1 f.lvl

One step

def Complexity.IPM.cmpBit (P : Params) (r : List Bool) : Bool

The verdict the walk finishes with: the count r exceeds half the coin space.

Equations

• Complexity.IPM.cmpBit P r = Complexity.ltBitsLE false (Complexity.twoPowBits P.t) (false :: r)

def Complexity.IPM.step (P : Params) (s : Sst) : Sst

One step of the walk.

Equations

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

@[simp]

theorem Complexity.IPM.step_of_done (P : Params) (a : Bool) (r : Option (List Bool)) (stk : List Frm) : step P { done := true, ansBit := a, ret := r, stk := stk } = { done := a, ansBit := a, ret := r, stk := stk }

@[simp]

theorem Complexity.IPM.step_of_empty (P : Params) (a : Bool) (r : Option (List Bool)) : step P { done := false, ansBit := a, ret := r, stk := [] } = { done := true, ansBit := cmpBit P (r.getD []), ret := r, stk := [] }

theorem Complexity.IPM.step_leaf_last (P : Params) (a : Bool) (f : Frm) (fs : List Frm) (hl : f.lvl = []) (hov : bumpOver f.a = true) : step P { done := false, ansBit := a, ret := none, stk := f :: fs } = { done := false, ansBit := a, ret := some (if P.ok (roundsOf fs) f.a = true then bumpBits f.sum else f.sum), stk := fs }

theorem Complexity.IPM.step_leaf_next (P : Params) (a : Bool) (f : Frm) (fs : List Frm) (hl : f.lvl = []) (hov : bumpOver f.a = false) : step P { done := false, ansBit := a, ret := none, stk := f :: fs } = { done := false, ansBit := a, ret := none, stk := { lvl := f.lvl, v := f.v, a := bumpBits f.a, sum := if P.ok (roundsOf fs) f.a = true then bumpBits f.sum else f.sum, best := f.best, body := f.body } :: fs }

theorem Complexity.IPM.step_push (P : Params) (a : Bool) (f : Frm) (fs : List Frm) (hl : f.lvl ≠ []) : step P { done := false, ansBit := a, ret := none, stk := f :: fs } = { done := false, ansBit := a, ret := none, stk := childFrm P f :: f :: fs }

theorem Complexity.IPM.step_ret_more_a (P : Params) (a : Bool) (f : Frm) (fs : List Frm) (r : List Bool) (ha : (nextStr f.a).length ≤ P.m) : step P { done := false, ansBit := a, ret := some r, stk := f :: fs } = { done := false, ansBit := a, ret := none, stk := { lvl := f.lvl, v := f.v, a := nextStr f.a, sum := f.sum, best := maxBits f.best r, body := f.body } :: fs }

theorem Complexity.IPM.step_ret_more_v (P : Params) (a : Bool) (f : Frm) (fs : List Frm) (r : List Bool) (ha : ¬(nextStr f.a).length ≤ P.m) (hv : (nextStr f.v).length ≤ P.m) : step P { done := false, ansBit := a, ret := some r, stk := f :: fs } = { done := false, ansBit := a, ret := none, stk := { lvl := f.lvl, v := nextStr f.v, a := [], sum := addBits f.sum (maxBits f.best r), best := zeroCount P, body := f.body } :: fs }

theorem Complexity.IPM.step_ret_pop (P : Params) (a : Bool) (f : Frm) (fs : List Frm) (r : List Bool) (ha : ¬(nextStr f.a).length ≤ P.m) (hv : ¬(nextStr f.v).length ≤ P.m) : step P { done := false, ansBit := a, ret := some r, stk := f :: fs } = { done := false, ansBit := a, ret := some (addBits f.sum (maxBits f.best r)), stk := fs }

The invariant the encoding needs

def Complexity.IPM.StkOk (s : Sst) : Prop

Nothing is returning only while the stack is nonempty.

Equations

• Complexity.IPM.StkOk s = (s.stk = [] → s.ret ≠ none)

theorem Complexity.IPM.step_stkOk (P : Params) {s : Sst} (h : StkOk s) : StkOk (step P s)

theorem Complexity.IPM.iterate_stkOk (P : Params) (j : ℕ) (s : Sst) : StkOk s → StkOk ((step P)^[j] s)

What the walk is computing

def Complexity.IPM.msgCount (P : Params) : ℕ

How many messages either side may send.

Equations

• Complexity.IPM.msgCount P = 2 ^ (P.m + 1) - 1

def Complexity.IPM.msgOf (i : ℕ) : List Bool

The i-th message in the enumeration.

Equations

• Complexity.IPM.msgOf i = Complexity.nextStr^[i] []

def Complexity.IPM.coinOf (P : Params) (k : ℕ) : List Bool

The k-th coin string.

Equations

• Complexity.IPM.coinOf P k = Complexity.bumpBits^[k] (Complexity.IPM.zeroCoin P)

def Complexity.IPM.treeVal (P : Params) : ℕ → List (List Bool × List Bool) → ℕ

What a node of the tree is worth: a count at a leaf, and a sum of maxima above.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.IPM.treeVal P 0 x✝ = {k ∈ Finset.range (2 ^ P.t) | P.ok x✝ (Complexity.IPM.coinOf P k) = true}.card

def Complexity.IPM.tailCol (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) (i ja : ℕ) : ℕ

The best the prover can do at the verifier's i-th message, from its ja-th reply on.

Equations

• Complexity.IPM.tailCol P n ps i ja = (Finset.Ico ja (Complexity.IPM.msgCount P)).sup fun (j : ℕ) => Complexity.IPM.treeVal P n (ps ++ [(Complexity.IPM.msgOf i, Complexity.IPM.msgOf j)])

def Complexity.IPM.col (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) (i : ℕ) : ℕ

The best the prover can do at the verifier's i-th message.

Equations

• Complexity.IPM.col P n ps i = Complexity.IPM.tailCol P n ps i 0

theorem Complexity.IPM.treeVal_zero (P : Params) (ps : List (List Bool × List Bool)) : treeVal P 0 ps = {k ∈ Finset.range (2 ^ P.t) | P.ok ps (coinOf P k) = true}.card

theorem Complexity.IPM.treeVal_succ (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) : treeVal P (n + 1) ps = ∑ i ∈ Finset.range (msgCount P), col P n ps i

Splitting off one step of a loop

theorem Complexity.IPM.Ico_eq_insert {a b : ℕ} (h : a < b) : Finset.Ico a b = insert a (Finset.Ico (a + 1) b)

theorem Complexity.IPM.tailCol_succ (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) (i ja : ℕ) (h : ja < msgCount P) : tailCol P n ps i ja = max (treeVal P n (ps ++ [(msgOf i, msgOf ja)])) (tailCol P n ps i (ja + 1))

theorem Complexity.IPM.tailCol_last (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) (i ja : ℕ) (h : msgCount P ≤ ja + 1) (h' : ja < msgCount P) : tailCol P n ps i ja = treeVal P n (ps ++ [(msgOf i, msgOf ja)])

theorem Complexity.IPM.tailCol_empty (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) (i ja : ℕ) (h : msgCount P ≤ ja) : tailCol P n ps i ja = 0

theorem Complexity.IPM.sum_col_split (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) (i : ℕ) (h : i < msgCount P) : ∑ k ∈ Finset.Ico i (msgCount P), col P n ps k = col P n ps i + ∑ k ∈ Finset.Ico (i + 1) (msgCount P), col P n ps k

theorem Complexity.IPM.sum_col_empty (P : Params) (n : ℕ) (ps : List (List Bool × List Bool)) (i : ℕ) (h : msgCount P ≤ i) : ∑ k ∈ Finset.Ico i (msgCount P), col P n ps k = 0

theorem Complexity.IPM.leaf_split (P : Params) (ps : List (List Bool × List Bool)) (k : ℕ) (h : k < 2 ^ P.t) : {l ∈ Finset.Ico k (2 ^ P.t) | P.ok ps (coinOf P l) = true}.card = (if P.ok ps (coinOf P k) = true then 1 else 0) + {l ∈ Finset.Ico (k + 1) (2 ^ P.t) | P.ok ps (coinOf P l) = true}.card

theorem Complexity.IPM.leaf_empty (P : Params) (ps : List (List Bool × List Bool)) (k : ℕ) (h : 2 ^ P.t ≤ k) : {l ∈ Finset.Ico k (2 ^ P.t) | P.ok ps (coinOf P l) = true}.card = 0

What a frame is still worth

theorem Complexity.IPM.msgOf_strIdx (w : List Bool) : msgOf (strIdx w) = w

@[simp]

theorem Complexity.IPM.strIdx_msgOf (i : ℕ) : strIdx (msgOf i) = i

theorem Complexity.IPM.coinOf_binValLE (P : Params) (s : List Bool) (hs : s.length = P.t) : coinOf P (binValLE s) = s

theorem Complexity.IPM.msgCount_pos (P : Params) : 0 < msgCount P

def Complexity.IPM.frameVal (P : Params) (ps : List (List Bool × List Bool)) (f : Frm) : ℕ

The value a frame will still contribute: what it has banked, plus what its loops have left to do.

Equations

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

theorem Complexity.IPM.frameVal_leaf (P : Params) (ps : List (List Bool × List Bool)) {f : Frm} (h : f.lvl = []) : frameVal P ps f = binValLE f.sum + {k ∈ Finset.Ico (binValLE f.a) (2 ^ P.t) | P.ok ps (coinOf P k) = true}.card

theorem Complexity.IPM.frameVal_branch (P : Params) (ps : List (List Bool × List Bool)) {f : Frm} {b : Bool} {t' : List Bool} (h : f.lvl = b :: t') : frameVal P ps f = binValLE f.sum + max (binValLE f.best) (tailCol P t'.length ps (strIdx f.v) (strIdx f.a)) + ∑ k ∈ Finset.Ico (strIdx f.v + 1) (msgCount P), col P t'.length ps k

theorem Complexity.IPM.frameVal_fresh (P : Params) (ps : List (List Bool × List Bool)) (body lvl : List Bool) : frameVal P ps (freshFrm P body lvl) = treeVal P lvl.length ps

A fresh frame is worth its whole subtree.

Runs

def Complexity.IPM.DoneDown (P : Params) (s : Sst) (T : ℕ) : Prop

The done flag is down at every point of the first T steps from s.

Equations

• Complexity.IPM.DoneDown P s T = ∀ j ≤ T, ((Complexity.IPM.step P)^[j] s).done = false

theorem Complexity.IPM.doneDown_zero (P : Params) {s : Sst} (h : s.done = false) : DoneDown P s 0

theorem Complexity.IPM.doneDown_add (P : Params) {s : Sst} {T₁ T₂ : ℕ} (h₁ : DoneDown P s T₁) (h₂ : DoneDown P ((step P)^[T₁] s) T₂) : DoneDown P s (T₁ + T₂)

theorem Complexity.IPM.doneDown_succ (P : Params) {s : Sst} {T : ℕ} (h : DoneDown P s T) (h' : ((step P)^[T + 1] s).done = false) : DoneDown P s (T + 1)

def Complexity.IPM.mu (P : Params) (f : Frm) : ℕ

How many loop iterations a frame still has to make.

Equations

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

def Complexity.IPM.runBound (P : Params) : ℕ → ℕ

The steps a frame at level n costs.

Equations

• Complexity.IPM.runBound P 0 = 2 ^ P.t
• Complexity.IPM.runBound P n.succ = Complexity.IPM.msgCount P * Complexity.IPM.msgCount P * (Complexity.IPM.runBound P n + 2)

theorem Complexity.IPM.runBound_pos (P : Params) (n : ℕ) : 0 < runBound P n

theorem Complexity.IPM.runBound_le (P : Params) (n : ℕ) : runBound P n + 2 ≤ 2 ^ (P.t + 2 + (2 * P.m + 3) * n)

The walk takes at most two to a polynomial steps.

structure Complexity.IPM.FrmOk (P : Params) (ps : List (List Bool × List Bool)) (f : Frm) : Prop

A frame is well formed when its registers have the right widths, its counters are inside the enumeration, and what it still owes fits in the coin space.

• sumLen : f.sum.length = P.t + 1

  The running sum has the count width.

• bestLen : f.best.length = P.t + 1

  So does the running maximum.

• coinLen : f.lvl = [] → f.a.length = P.t

  A leaf's coin counter has the coin width.

• vIdx : f.lvl ≠ [] → strIdx f.v < msgCount P

  A branch's verifier counter is inside the enumeration.

• aIdx : f.lvl ≠ [] → strIdx f.a < msgCount P

  So is its prover counter.

• bnd : frameVal P ps f ≤ 2 ^ P.t

  What the frame still owes fits in the coin space.

def Complexity.IPM.RunsTo (P : Params) (f : Frm) (fs : List Frm) (a : Bool) (T : ℕ) : Prop

The frame f, pushed on fs, is popped again carrying its value after exactly T steps, and the done flag stays down for the whole of that run.

Equations

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

theorem Complexity.IPM.runsTo_prepend (P : Params) {f g : Frm} {fs : List Frm} {a : Bool} {T₀ T₁ : ℕ} (hd : DoneDown P { done := false, ansBit := a, ret := none, stk := f :: fs } T₀) (hs : (step P)^[T₀] { done := false, ansBit := a, ret := none, stk := f :: fs } = { done := false, ansBit := a, ret := none, stk := g :: fs }) (hr : RunsTo P g fs a T₁) (hval : frameVal P (roundsOf fs) g = frameVal P (roundsOf fs) f) : RunsTo P f fs a (T₁ + T₀)

A run that begins by re-entering a frame of the same value.

theorem Complexity.IPM.mu_leaf (P : Params) {f : Frm} (h : f.lvl = []) : mu P f = 2 ^ P.t - binValLE f.a

theorem Complexity.IPM.mu_branch (P : Params) {f : Frm} {b : Bool} {t' : List Bool} (h : f.lvl = b :: t') : mu P f = (msgCount P - 1 - strIdx f.v) * msgCount P + (msgCount P - strIdx f.a)

theorem Complexity.IPM.run_leaf (P : Params) (M : ℕ) (f : Frm) : mu P f ≤ M → f.lvl = [] → ∀ (fs : List Frm), FrmOk P (roundsOf fs) f → ∀ (a : Bool), ∃ T ≤ mu P f, RunsTo P f fs a T

A leaf runs its coin loop and pops with the tally.

theorem Complexity.IPM.child_phase (P : Params) {f : Frm} {fs : List Frm} {a : Bool} {Tc : ℕ} {w : List Bool} {s : Sst} (hne : f.lvl ≠ []) (hdd : DoneDown P { done := false, ansBit := a, ret := none, stk := childFrm P f :: f :: fs } Tc) (hend : (step P)^[Tc] { done := false, ansBit := a, ret := none, stk := childFrm P f :: f :: fs } = { done := false, ansBit := a, ret := some w, stk := f :: fs }) (hstep : step P { done := false, ansBit := a, ret := some w, stk := f :: fs } = s) (hsdone : s.done = false) : DoneDown P { done := false, ansBit := a, ret := none, stk := f :: fs } (Tc + 1 + 1) ∧ (step P)^[Tc + 1 + 1] { done := false, ansBit := a, ret := none, stk := f :: fs } = s

Pushing a subtree, running it, and processing the value it returns.

theorem Complexity.IPM.run_branch (P : Params) (hval : ∀ (n : ℕ) (ps : List (List Bool × List Bool)), treeVal P n ps ≤ 2 ^ P.t) (n : ℕ) (ih : ∀ (g : Frm), g.lvl.length = n → ∀ (gs : List Frm), FrmOk P (roundsOf gs) g → ∀ (b : Bool), ∃ T ≤ runBound P n, RunsTo P g gs b T) (M : ℕ) (f : Frm) : mu P f ≤ M → f.lvl.length = n + 1 → ∀ (fs : List Frm), FrmOk P (roundsOf fs) f → ∀ (a : Bool), ∃ T ≤ mu P f * (runBound P n + 2), RunsTo P f fs a T

A branch runs both of its loops and pops with the sum.

theorem Complexity.IPM.frmOk_fresh (P : Params) (hval : ∀ (n : ℕ) (ps : List (List Bool × List Bool)), treeVal P n ps ≤ 2 ^ P.t) (ps : List (List Bool × List Bool)) (body lvl : List Bool) : FrmOk P ps (freshFrm P body lvl)

A fresh frame is well formed.

theorem Complexity.IPM.run_frame (P : Params) (hval : ∀ (n : ℕ) (ps : List (List Bool × List Bool)), treeVal P n ps ≤ 2 ^ P.t) (n : ℕ) (f : Frm) : f.lvl.length = n → ∀ (fs : List Frm), FrmOk P (roundsOf fs) f → ∀ (a : Bool), ∃ T ≤ runBound P n, RunsTo P f fs a T

Every pushed frame comes back, carrying its value, within runBound steps.

theorem Complexity.IPM.run_top (P : Params) (hval : ∀ (n : ℕ) (ps : List (List Bool × List Bool)), treeVal P n ps ≤ 2 ^ P.t) (lvl : List Bool) : ∃ (T : ℕ) (w : List Bool), T ≤ runBound P lvl.length ∧ w.length = P.t + 1 ∧ binValLE w = treeVal P lvl.length [] ∧ (∀ j ≤ T, ((step P)^[j] { done := false, ansBit := false, ret := none, stk := [freshFrm P [] lvl] }).done = false) ∧ (step P)^[T + 1] { done := false, ansBit := false, ret := none, stk := [freshFrm P [] lvl] } = { done := true, ansBit := cmpBit P w, ret := some w, stk := [] } ∧ (step P)^[T + 2] { done := false, ansBit := false, ret := none, stk := [freshFrm P [] lvl] } = { done := cmpBit P w, ansBit := cmpBit P w, ret := some w, stk := [] }

The whole walk. From a single fresh frame the machine keeps its flag down, raises it on the next step, and one step later the flag is the verdict.