The leaf test

⚠️ Unreviewed by Bolton

At a leaf the walk asks one question of each coin string: would the verifier have sent every message the transcript records, and does it accept? The first half is Complexity.Protocol.replay, which walks the rounds in play order carrying the encoding body with it — the wrong direction for a stack, whose top frame is the last round.

Carrying each frame's body inside the frame removes the problem: the check a round contributes depends only on that round's verifier message and its own body, so the conjunction may be taken in any order. That is what Complexity.stkCheckB does, and it is what a scan over the encoded stack can compute.

Main definitions

• Complexity.stkCheckB — the per-frame form of the consistency test

Main results

• Complexity.Protocol.replay_append — a round appended checks its own message last
• Complexity.replay_eq_stkCheckB — the two forms agree

theorem Complexity.Protocol.replay_append (prot : Protocol) (x s : List Bool) (ps : List (List Bool × List Bool)) (p : List Bool × List Bool) (body : List Bool) : prot.replay x s (ps ++ [p]) body = (prot.replay x s ps body && decide (p.1 = prot.vmsg (pair (pair x s) (false :: (body ++ encBodyR ps) ++ [true]))))

A round appended checks its own message last, against the body of everything before it.

def Complexity.stkCheckB (vf : List Bool → List Bool) (x s : List Bool) : List IPM.Frm → Bool

The consistency test as a conjunction over the frames, each checking its own recorded message against its own body.

Equations

• Complexity.stkCheckB vf x s [] = true
• Complexity.stkCheckB vf x s (g :: gs) = (decide (g.v = vf (Complexity.pair (Complexity.pair x s) (false :: g.body ++ [true]))) && Complexity.stkCheckB vf x s gs)

@[simp]

theorem Complexity.stkCheckB_nil (vf : List Bool → List Bool) (x s : List Bool) : stkCheckB vf x s [] = true

theorem Complexity.stkCheckB_cons (vf : List Bool → List Bool) (x s : List Bool) (g : IPM.Frm) (gs : List IPM.Frm) : stkCheckB vf x s (g :: gs) = (decide (g.v = vf (pair (pair x s) (false :: g.body ++ [true]))) && stkCheckB vf x s gs)

theorem Complexity.replay_eq_stkCheckB (prot : Protocol) (x s : List Bool) (fs : List IPM.Frm) : IPM.BodyOk fs → prot.replay x s (IPM.roundsOf fs) [] = stkCheckB prot.vmsg x s fs

The two forms of the consistency test agree.

Flags as decisions

theorem Complexity.eqFlag_eq_decide (a b : List Bool) : Cobham.eqFlag a b = [decide (a = b)]

@[simp]

theorem Complexity.andBit_cons (b c : Bool) : andBit [b] [c] = [b && c]

theorem Complexity.andBit_length_eq (u v : List Bool) : (andBit u v).length = 1

The scan over the stack

def Complexity.chkOneP (vf : List Bool → List Bool) (xu y : List Bool) : List Bool

The check one frame contributes, on the tape.

Equations

• Complexity.chkOneP vf xu y = Complexity.Cobham.eqFlag (Complexity.IPM.fV y) (vf (Complexity.pair xu (false :: Complexity.IPM.fBody y ++ [true])))

theorem Complexity.chkOneP_enc (vf : List Bool → List Bool) (xu : List Bool) (g : IPM.Frm) : chkOneP vf xu (IPM.encFrm g) = [decide (g.v = vf (pair xu (false :: g.body ++ [true])))]

def Complexity.chkStep (vf : List Bool → List Bool) : List Bool × List Bool × List Bool → List Bool × List Bool × List Bool

One step of the scan: fold the next frame's check into the running flag.

Equations

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

@[simp]

theorem Complexity.chkStep_nil (vf : List Bool → List Bool) (xu acc : List Bool) : chkStep vf (xu, acc, []) = (xu, acc, [])

theorem Complexity.chkStep_cons (vf : List Bool → List Bool) (xu acc : List Bool) (g : IPM.Frm) (gs : List IPM.Frm) : chkStep vf (xu, acc, IPM.encStk (g :: gs)) = (xu, andBit acc (chkOneP vf xu (IPM.encFrm g)), IPM.encStk gs)

def Complexity.chkFold (vf : List Bool → List Bool) (xu : List Bool) : List Bool → List IPM.Frm → List Bool

The running flag after folding in a list of frames.

Equations

• Complexity.chkFold vf xu x✝ [] = x✝
• Complexity.chkFold vf xu x✝ (g :: gs) = Complexity.chkFold vf xu (Complexity.andBit x✝ (Complexity.chkOneP vf xu (Complexity.IPM.encFrm g))) gs

theorem Complexity.chkFold_flag (vf : List Bool → List Bool) (x u : List Bool) (fs : List IPM.Frm) (b : Bool) : chkFold vf (pair x u) [b] fs = [b && stkCheckB vf x u fs]

theorem Complexity.chkStep_iterate (vf : List Bool → List Bool) (xu : List Bool) (fs : List IPM.Frm) (acc : List Bool) (n : ℕ) : fs.length ≤ n → (chkStep vf)^[n] (xu, acc, IPM.encStk fs) = (xu, chkFold vf xu acc fs, [])

The scan folds every frame in.

The packed scan

theorem Complexity.sndBlock_length_le (z : List Bool) : (pairSnd z).length ≤ z.length

def Complexity.chkPack (xu acc S : List Bool) : List Bool

The packed scan state: the verifier's fixed arguments, the running flag, and the chain of frames still to check.

Equations

• Complexity.chkPack xu acc S = Complexity.pair xu (Complexity.pair acc S)

@[simp]

theorem Complexity.chkPack_length (xu acc S : List Bool) : (chkPack xu acc S).length = 2 * xu.length + 2 * acc.length + S.length + 4

def Complexity.chkStepP (vf : List Bool → List Bool) (z : List Bool) : List Bool

One step of the packed scan.

Equations

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

theorem Complexity.chkStepP_pack (vf : List Bool → List Bool) (xu acc S : List Bool) : chkStepP vf (chkPack xu acc S) = chkPack (chkStep vf (xu, acc, S)).1 (chkStep vf (xu, acc, S)).2.1 (chkStep vf (xu, acc, S)).2.2

theorem Complexity.chkStepP_iterate (vf : List Bool → List Bool) (s : List Bool × List Bool × List Bool) (n : ℕ) : (chkStepP vf)^[n] (chkPack s.1 s.2.1 s.2.2) = chkPack ((chkStep vf)^[n] s).1 ((chkStep vf)^[n] s).2.1 ((chkStep vf)^[n] s).2.2

theorem Complexity.chkStepP_iterate_args (vf : List Bool → List Bool) (xu acc S : List Bool) (n : ℕ) : (chkStepP vf)^[n] (chkPack xu acc S) = chkPack ((chkStep vf)^[n] (xu, acc, S)).1 ((chkStep vf)^[n] (xu, acc, S)).2.1 ((chkStep vf)^[n] (xu, acc, S)).2.2

theorem Complexity.chkStep_iterate_length (vf : List Bool → List Bool) (xu acc S : List Bool) (n : ℕ) : ((chkStep vf)^[n] (xu, acc, S)).1 = xu ∧ ((chkStep vf)^[n] (xu, acc, S)).2.1.length ≤ max acc.length 1 ∧ ((chkStep vf)^[n] (xu, acc, S)).2.2.length ≤ S.length

The leaf test

def Complexity.chkFlag (vf : List Bool → List Bool) (rr xu S : List Bool) : List Bool

The consistency flag, computed by running the scan against a ruler.

Equations

• Complexity.chkFlag vf rr xu S = Complexity.pairFst (Complexity.pairSnd ((Complexity.chkStepP vf)^[rr.length] (Complexity.chkPack xu [true] S)))

theorem Complexity.chkFlag_eq (vf : List Bool → List Bool) (rr x u : List Bool) (fs : List IPM.Frm) (h : fs.length ≤ rr.length) : chkFlag vf rr (pair x u) (IPM.encStk fs) = [stkCheckB vf x u fs]

def Complexity.okFn (vf vd : List Bool → List Bool) (rr x S u : List Bool) : List Bool

The leaf test on the tape: the transcript replays, and the verifier accepts.

Equations

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

theorem Complexity.okFn_eq (prot : Protocol) (vd : List Bool → List Bool) (hvd : ∀ (z : List Bool), vd z = [decide (z ∈ prot.verdict)]) (rr x u : List Bool) (f : IPM.Frm) (fs : List IPM.Frm) (hb : IPM.BodyOk (f :: fs)) (hlen : fs.length ≤ rr.length) : okFn prot.vmsg vd rr x (IPM.encStk (f :: fs)) u = [(prot.walkParams x).ok (IPM.roundsOf fs) u]

The leaf test computes what the walk asks for.

The leaf test is polynomial-time

theorem Complexity.chkOnePFn_mem_FP {vf : List Bool → List Bool} (hvf : vf ∈ FP) {XU Y : List Bool → List Bool} (hxu : XU ∈ FP) (hy : Y ∈ FP) : (fun (z : List Bool) => chkOneP vf (XU z) (Y z)) ∈ FP

theorem Complexity.chkStepPFn_mem_FP {vf : List Bool → List Bool} (hvf : vf ∈ FP) : chkStepP vf ∈ FP

theorem Complexity.chkFlagFn_mem_FP {vf : List Bool → List Bool} (hvf : vf ∈ FP) {R XU S : List Bool → List Bool} (hR : R ∈ FP) (hxu : XU ∈ FP) (hS : S ∈ FP) : (fun (z : List Bool) => chkFlag vf (R z) (XU z) (S z)) ∈ FP

theorem Complexity.okFnFn_mem_FP {vf vd : List Bool → List Bool} (hvf : vf ∈ FP) (hvd : vd ∈ FP) {R X S U : List Bool → List Bool} (hR : R ∈ FP) (hX : X ∈ FP) (hS : S ∈ FP) (hU : U ∈ FP) : (fun (z : List Bool) => okFn vf vd (R z) (X z) (S z) (U z)) ∈ FP

The leaf test discharges the walk's hypothesis

theorem Complexity.exists_verdictFlag (prot : Protocol) : ∃ vd ∈ FP, ∀ (z : List Bool), vd z = [decide (z ∈ prot.verdict)]

The verifier's verdict as a one-bit flag.

theorem Complexity.okFn_hokf (prot : Protocol) (vd : List Bool → List Bool) (hvd : ∀ (z : List Bool), vd z = [decide (z ∈ prot.verdict)]) (rr x : List Bool) (D : ℕ) (hD : D ≤ rr.length + 1) (f : IPM.Frm) (fs : List IPM.Frm) : IPM.BodyOk (f :: fs) → (f :: fs).length ≤ D → ∀ (u : List Bool), okFn prot.vmsg vd rr x (IPM.encStk (f :: fs)) u = [(prot.walkParams x).ok (IPM.roundsOf fs) u]

The leaf test is exactly what the walk asks for, for every stack the walk can reach.