The walk's state on a bitstring

⚠️ Unreviewed by Bolton

Complexitylib.Classes.Containments.Internal.IPSem walks the game tree on an inductive state. A machine has to hold that state on a tape, so this file writes it as a bitstring — a frame is five blocks, the stack a right-nested chain of pairs — and records the invariant the encoding needs: a returning value is a count, so it is never empty, which is what tells some from none.

Main definitions

• Complexity.IPM.encFrm, Complexity.IPM.encStk, Complexity.IPM.encSst — the encoding
• Complexity.IPM.EncOk — the invariant the encoding relies on

Main results

• Complexity.IPM.step_encOk — the invariant is preserved

The encoding

def Complexity.IPM.encFrm (f : Frm) : List Bool

A frame on the tape: five blocks.

Equations

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

def Complexity.IPM.encStk : List Frm → List Bool

The stack on the tape: a right-nested chain of pairs, empty stack being the empty string.

Equations

• Complexity.IPM.encStk [] = []
• Complexity.IPM.encStk (f :: fs) = Complexity.pair (Complexity.IPM.encFrm f) (Complexity.IPM.encStk fs)

@[simp]

theorem Complexity.IPM.encStk_nil : encStk [] = []

@[simp]

theorem Complexity.IPM.encStk_cons (f : Frm) (fs : List Frm) : encStk (f :: fs) = pair (encFrm f) (encStk fs)

def Complexity.IPM.encRet : Option (List Bool) → List Bool

A returning value on the tape. A count is never empty, so the empty string means nothing is returning.

Equations

• Complexity.IPM.encRet none = []
• Complexity.IPM.encRet (some w) = w

@[simp]

theorem Complexity.IPM.encRet_none : encRet none = []

@[simp]

theorem Complexity.IPM.encRet_some (w : List Bool) : encRet (some w) = w

def Complexity.IPM.encSst (s : Sst) : List Bool

The state on the tape.

Equations

• Complexity.IPM.encSst s = Complexity.pair [s.done] (Complexity.pair [s.ansBit] (Complexity.pair (Complexity.IPM.encRet s.ret) (Complexity.IPM.encStk s.stk)))

theorem Complexity.IPM.encSst_ne_nil (s : Sst) : encSst s ≠ []

theorem Complexity.IPM.encSst_headD (s : Sst) : (encSst s).headD false = s.done

theorem Complexity.IPM.headD_pair_encSst (s : Sst) (x : List Bool) : (pair (encSst s) x).headD false = s.done

The invariant the encoding relies on

def Complexity.IPM.BodyOk : List Frm → Prop

Every frame carries the body of the rounds below it.

Equations

• Complexity.IPM.BodyOk [] = True
• Complexity.IPM.BodyOk (f :: fs) = (f.body = Complexity.encBodyR (Complexity.IPM.roundsOf fs) ∧ Complexity.IPM.BodyOk fs)

@[simp]

theorem Complexity.IPM.bodyOk_nil : BodyOk []

theorem Complexity.IPM.bodyOk_cons {f : Frm} {fs : List Frm} (h : f.body = encBodyR (roundsOf fs)) (h' : BodyOk fs) : BodyOk (f :: fs)

def Complexity.IPM.StkDepth (D : ℕ) : List Frm → Prop

The stack descends exactly one level per frame, so its depth is the level it started at.

Equations

• Complexity.IPM.StkDepth D [] = True
• Complexity.IPM.StkDepth D (f :: fs) = (fs.length + f.lvl.length + 1 = D ∧ Complexity.IPM.StkDepth D fs)

theorem Complexity.IPM.StkDepth.length_le {D : ℕ} {stk : List Frm} : StkDepth D stk → stk.length ≤ D

structure Complexity.IPM.EncOk (P : Params) (D : ℕ) (s : Sst) : Prop

The encoding is faithful when nothing is returning while the stack is empty, and every count on the state has the width a count is held in — so that a returning value is never empty.

• stkOk : s.stk = [] → s.ret ≠ none

  Nothing returns to an empty stack.

• retLen (w : List Bool) : s.ret = some w → w.length = P.t + 1

  A returning value is a count.

• frmLen (f : Frm) : f ∈ s.stk → f.sum.length = P.t + 1 ∧ f.best.length = P.t + 1

  So are the accumulators on the stack.

• bodyOk : BodyOk s.stk

  Every frame carries the body of the rounds below it.

• depthOk : StkDepth D s.stk

  The stack is no deeper than the level it started at.

theorem Complexity.IPM.encRet_ne_nil {P : Params} {D : ℕ} {s : Sst} (h : EncOk P D s) {w : List Bool} (hw : s.ret = some w) : w ≠ []

theorem Complexity.IPM.zeroCount_length (P : Params) : (zeroCount P).length = P.t + 1

theorem Complexity.IPM.freshFrm_len (P : Params) (body lvl : List Bool) : (freshFrm P body lvl).sum.length = P.t + 1 ∧ (freshFrm P body lvl).best.length = P.t + 1

theorem Complexity.IPM.step_encOk (P : Params) (D : ℕ) {s : Sst} (h : EncOk P D s) : EncOk P D (step P s)

The invariant is preserved.

theorem Complexity.IPM.iterate_encOk (P : Params) (D j : ℕ) (s : Sst) : EncOk P D s → EncOk P D ((step P)^[j] s)

theorem Complexity.IPM.encOk_start (P : Params) (lvl : List Bool) : EncOk P (lvl.length + 1) { done := false, ansBit := false, ret := none, stk := [freshFrm P [] lvl] }

How long an encoded state is

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

The width a message counter can reach.

Equations

• Complexity.IPM.msgW P = max P.m P.t

def Complexity.IPM.SizeOk (P : Params) : List Frm → Prop

Every frame's counters are within the widths the walk uses.

Equations

• Complexity.IPM.SizeOk P [] = True
• Complexity.IPM.SizeOk P (f :: fs) = (f.v.length ≤ P.m ∧ f.a.length ≤ Complexity.IPM.msgW P ∧ Complexity.IPM.SizeOk P fs)

theorem Complexity.IPM.step_sizeOk (P : Params) {s : Sst} (h : SizeOk P s.stk) : SizeOk P (step P s).stk

theorem Complexity.IPM.iterate_sizeOk (P : Params) (j : ℕ) (s : Sst) : SizeOk P s.stk → SizeOk P ((step P)^[j] s).stk

theorem Complexity.IPM.sizeOk_start (P : Params) (lvl : List Bool) : SizeOk P [freshFrm P [] lvl]

theorem Complexity.IPM.body_length_le (P : Params) (fs : List Frm) : SizeOk P fs → (encBodyR (roundsOf fs)).length ≤ fs.length * (8 * msgW P + 4)

The transcript body a stack records is polynomially long.

theorem Complexity.IPM.encFrm_length_le (P : Params) (D B : ℕ) (f : Frm) (hl : f.lvl.length + 1 ≤ D) (hv : f.v.length ≤ P.m) (ha : f.a.length ≤ msgW P) (hs : f.sum.length = P.t + 1) (hb : f.best.length = P.t + 1) (hbody : f.body.length ≤ B) : (encFrm f).length ≤ 2 * D + 2 * P.m + 2 * msgW P + 4 * (P.t + 1) + B + 10

theorem Complexity.IPM.encStk_length_le (fs : List Frm) (B : ℕ) : (∀ g ∈ fs, (encFrm g).length ≤ B) → (encStk fs).length ≤ fs.length * (2 * B + 2)

theorem Complexity.IPM.StkDepth.mem_le {D : ℕ} {stk : List Frm} : StkDepth D stk → ∀ f ∈ stk, f.lvl.length + 1 ≤ D

theorem Complexity.IPM.SizeOk.mem {P : Params} {stk : List Frm} : SizeOk P stk → ∀ f ∈ stk, f.v.length ≤ P.m ∧ f.a.length ≤ msgW P

theorem Complexity.IPM.SizeOk.tail {P : Params} {g : Frm} {gs : List Frm} (h : SizeOk P (g :: gs)) : SizeOk P gs

theorem Complexity.IPM.body_bound_mem (P : Params) (D : ℕ) (stk : List Frm) : BodyOk stk → SizeOk P stk → StkDepth D stk → ∀ g ∈ stk, g.body.length ≤ D * (8 * msgW P + 4)

def Complexity.IPM.stateBound (P : Params) (D : ℕ) : ℕ

The width the encoded state stays inside.

Equations

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

theorem Complexity.IPM.stateBound_le (P : Params) (D M : ℕ) (hM : msgW P ≤ M) : stateBound P D ≤ 2 * (P.t + 1) + D * (2 * (2 * D + 2 * P.m + 2 * M + 4 * (P.t + 1) + D * (8 * M + 4) + 10) + 2) + 10

theorem Complexity.IPM.encSst_length_le (P : Params) (D : ℕ) (s : Sst) (h : EncOk P D s) (hsz : SizeOk P s.stk) : (encSst s).length ≤ stateBound P D

An encoded state is polynomially long.