One step of the walk, inside the polynomial-time algebra

⚠️ Unreviewed by Bolton

Complexity.IPM.step walks the game tree on an inductive state; Complexity.IPM.encSst writes that state on a tape. This file writes the step on the tape, out of the algebra's operations only, and proves the square commutes.

Everything the step needs from the protocol enters through three arguments: a ruler mr whose length is the message bound, a ruler cr whose length is the coin width, and the leaf test okf, which reads the encoded stack below a leaf and a coin string.

Main definitions

• Complexity.IPM.ipStep — the encoded step
• Complexity.IPM.freshEnc — the frame a node starts from, on the tape

Main results

• Complexity.IPM.ipStep_encSst — one encoded step is one abstract step
• Complexity.IPM.ipStepFn_mem_FP — and it is polynomial-time

Reading and writing the encoded state

def Complexity.IPM.mkS (d ab r stk : List Bool) : List Bool

The state's four fields, written.

Equations

• Complexity.IPM.mkS d ab r stk = Complexity.pair d (Complexity.pair ab (Complexity.pair r stk))

def Complexity.IPM.mkF (lvl v a sum best body : List Bool) : List Bool

A frame's six fields, written.

Equations

• Complexity.IPM.mkF lvl v a sum best body = Complexity.pair lvl (Complexity.pair v (Complexity.pair a (Complexity.pair sum (Complexity.pair best body))))

@[simp]

theorem Complexity.IPM.mkS_eq (s : Sst) : mkS [s.done] [s.ansBit] (encRet s.ret) (encStk s.stk) = encSst s

@[simp]

theorem Complexity.IPM.mkF_eq (f : Frm) : mkF f.lvl f.v f.a f.sum f.best f.body = encFrm f

def Complexity.IPM.sDone (z : List Bool) : List Bool

The done flag.

Equations

• Complexity.IPM.sDone z = Complexity.pairFst z

def Complexity.IPM.sAns (z : List Bool) : List Bool

The answer bit.

Equations

• Complexity.IPM.sAns z = Complexity.pairFst (Complexity.pairSnd z)

def Complexity.IPM.sRet (z : List Bool) : List Bool

The returning value.

Equations

• Complexity.IPM.sRet z = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd z))

def Complexity.IPM.sStk (z : List Bool) : List Bool

The stack.

Equations

• Complexity.IPM.sStk z = Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd z))

def Complexity.IPM.fLvl (y : List Bool) : List Bool

A frame's level.

Equations

• Complexity.IPM.fLvl y = Complexity.pairFst y

def Complexity.IPM.fV (y : List Bool) : List Bool

A frame's verifier counter.

Equations

• Complexity.IPM.fV y = Complexity.pairFst (Complexity.pairSnd y)

def Complexity.IPM.fA (y : List Bool) : List Bool

A frame's prover counter, or its coin counter.

Equations

• Complexity.IPM.fA y = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd y))

def Complexity.IPM.fSum (y : List Bool) : List Bool

A frame's running sum.

Equations

• Complexity.IPM.fSum y = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd y)))

def Complexity.IPM.fBest (y : List Bool) : List Bool

A frame's running maximum.

Equations

• Complexity.IPM.fBest y = Complexity.pairFst (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd y))))

def Complexity.IPM.fBody (y : List Bool) : List Bool

The body of the encoding of the rounds below a frame.

Equations

• Complexity.IPM.fBody y = Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd (Complexity.pairSnd y))))

def Complexity.IPM.sTop (S : List Bool) : List Bool

The frame on top of the stack.

Equations

• Complexity.IPM.sTop S = Complexity.pairFst S

def Complexity.IPM.sRest (S : List Bool) : List Bool

The stack below the top frame.

Equations

• Complexity.IPM.sRest S = Complexity.pairSnd S

@[simp]

theorem Complexity.IPM.sDone_enc (s : Sst) : sDone (encSst s) = [s.done]

@[simp]

theorem Complexity.IPM.sAns_enc (s : Sst) : sAns (encSst s) = [s.ansBit]

@[simp]

theorem Complexity.IPM.sRet_enc (s : Sst) : sRet (encSst s) = encRet s.ret

@[simp]

theorem Complexity.IPM.sStk_enc (s : Sst) : sStk (encSst s) = encStk s.stk

@[simp]

theorem Complexity.IPM.fLvl_enc (f : Frm) : fLvl (encFrm f) = f.lvl

@[simp]

theorem Complexity.IPM.fV_enc (f : Frm) : fV (encFrm f) = f.v

@[simp]

theorem Complexity.IPM.fA_enc (f : Frm) : fA (encFrm f) = f.a

@[simp]

theorem Complexity.IPM.fSum_enc (f : Frm) : fSum (encFrm f) = f.sum

@[simp]

theorem Complexity.IPM.fBest_enc (f : Frm) : fBest (encFrm f) = f.best

@[simp]

theorem Complexity.IPM.fBody_enc (f : Frm) : fBody (encFrm f) = f.body

@[simp]

theorem Complexity.IPM.sTop_pair (y S : List Bool) : sTop (pair y S) = y

@[simp]

theorem Complexity.IPM.sRest_pair (y S : List Bool) : sRest (pair y S) = S

theorem Complexity.IPM.sTop_cons (f : Frm) (fs : List Frm) : sTop (encStk (f :: fs)) = encFrm f

theorem Complexity.IPM.sRest_cons (f : Frm) (fs : List Frm) : sRest (encStk (f :: fs)) = encStk fs

The encoded step

def Complexity.IPM.zcOf (cr : List Bool) : List Bool

The zero of a count's width, from the coin ruler.

Equations

• Complexity.IPM.zcOf cr = Complexity.padTo (cr ++ [false]) []

def Complexity.IPM.zkOf (cr : List Bool) : List Bool

The first coin string, from the coin ruler.

Equations

• Complexity.IPM.zkOf cr = Complexity.padTo cr []

def Complexity.IPM.tpOf (cr : List Bool) : List Bool

The bitstring of 2 ^ t, from the coin ruler.

Equations

• Complexity.IPM.tpOf cr = Complexity.padTo cr [] ++ [true, false]

theorem Complexity.IPM.zcOf_eq (cr : List Bool) (P : Params) (h : cr.length = P.t) : zcOf cr = zeroCount P

theorem Complexity.IPM.zkOf_eq (cr : List Bool) (P : Params) (h : cr.length = P.t) : zkOf cr = zeroCoin P

theorem Complexity.IPM.tpOf_eq (cr : List Bool) (P : Params) (h : cr.length = P.t) : tpOf cr = twoPowBits P.t

def Complexity.IPM.freshEnc (cr body lvl : List Bool) : List Bool

The frame a node starts from, written on the tape.

Equations

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

theorem Complexity.IPM.freshEnc_eq (cr : List Bool) (P : Params) (h : cr.length = P.t) (body lvl : List Bool) : freshEnc cr body lvl = encFrm (freshFrm P body lvl)

def Complexity.IPM.ipDescend (cr : List Bool) (okf : List Bool → List Bool → List Bool) (z : List Bool) : List Bool

The descending half of the step: a leaf tallies one coin string, a branch pushes a subtree.

Equations

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

def Complexity.IPM.ipReturn (mr cr z : List Bool) : List Bool

The returning half of the step: advance a counter, or pop with the sum.

Equations

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

def Complexity.IPM.ipStep (mr cr : List Bool) (okf : List Bool → List Bool → List Bool) (z : List Bool) : List Bool

One step of the walk, on the tape.

Equations

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

def Complexity.IPM.ipInit (cr rr : List Bool) : List Bool

The state the walk starts from, on the tape.

Equations

• Complexity.IPM.ipInit cr rr = Complexity.IPM.mkS [false] [false] [] (Complexity.pair (Complexity.IPM.freshEnc cr [] rr) [])

theorem Complexity.IPM.ipInit_eq (cr : List Bool) (P : Params) (h : cr.length = P.t) (rr : List Bool) : ipInit cr rr = encSst { done := false, ansBit := false, ret := none, stk := [freshFrm P [] rr] }

theorem Complexity.IPM.ipInitFn_mem_FP {CR RR : List Bool → List Bool} (hcr : CR ∈ FP) (hrr : RR ∈ FP) : (fun (z : List Bool) => ipInit (CR z) (RR z)) ∈ FP

The square commutes

theorem Complexity.IPM.lenLeFlag_true (mr u : List Bool) (h : u.length ≤ mr.length) : Cobham.lenLeFlag mr u = [true]

theorem Complexity.IPM.lenLeFlag_false (mr u : List Bool) (h : ¬u.length ≤ mr.length) : Cobham.lenLeFlag mr u = [false]

theorem Complexity.IPM.ipStep_encSst (P : Params) (mr cr : List Bool) (hm : mr.length = P.m) (hc : cr.length = P.t) (okf : List Bool → List Bool → List Bool) (D : ℕ) (hokf : ∀ (f : Frm) (fs : List Frm), BodyOk (f :: fs) → (f :: fs).length ≤ D → ∀ (u : List Bool), okf (encStk (f :: fs)) u = [P.ok (roundsOf fs) u]) (s : Sst) (h : EncOk P D s) : ipStep mr cr okf (encSst s) = encSst (step P s)

One encoded step is one abstract step.

theorem Complexity.IPM.ipStep_iterate (P : Params) (mr cr : List Bool) (hm : mr.length = P.m) (hc : cr.length = P.t) (okf : List Bool → List Bool → List Bool) (D : ℕ) (hokf : ∀ (f : Frm) (fs : List Frm), BodyOk (f :: fs) → (f :: fs).length ≤ D → ∀ (u : List Bool), okf (encStk (f :: fs)) u = [P.ok (roundsOf fs) u]) (j : ℕ) (s : Sst) : EncOk P D s → (ipStep mr cr okf)^[j] (encSst s) = encSst ((step P)^[j] s)

And so is any number of steps.

The encoded step is polynomial-time

theorem Complexity.IPM.ipStepFn_mem_FP {A B C : List Bool → List Bool} (hA : A ∈ FP) (hB : B ∈ FP) (hC : C ∈ FP) {OK : List Bool → List Bool → List Bool → List Bool} (hok : ∀ {u v : List Bool → List Bool}, u ∈ FP → v ∈ FP → (fun (z : List Bool) => OK z (u z) (v z)) ∈ FP) : (fun (z : List Bool) => ipStep (A z) (B z) (OK z) (C z)) ∈ FP