The closure library, part VI: the bits of a tree

The preorder serialization Data.toBits of a tree, as a program (toBitsProg, a stack-driven traversal after sizeProg) and as a polynomial-time function (PolyTimeFun.toBits). This is how the describer of the succinct Cook–Levin theorem obtains the symbol strings of the interpreter machine's fixed input tapes — S d = bits d.toBits — from the data d (planning/succinct-cook-levin.md, S3).

def MIPRE.Cost.Prog.tbStop : Prog

Body of toBitsProg: the state is cons stack acc, stack a list of pending subtrees and acc the bits produced so far, reversed. Pop a subtree: nil emits 0; cons a b emits 1 and pushes a then b. Stop with acc when the stack is empty.

Equations

• MIPRE.Cost.Prog.tbStop = MIPRE.Cost.Prog.nil.cons (MIPRE.Cost.Prog.var 1)

def MIPRE.Cost.Prog.tbNil : Prog

The step on a nil subtree: emit 0.

Equations

• MIPRE.Cost.Prog.tbNil = (MIPRE.Cost.Prog.nil.cons MIPRE.Cost.Prog.nil).cons ((MIPRE.Cost.Prog.var 1).cons (MIPRE.Cost.Prog.nil.cons (MIPRE.Cost.Prog.var 3)))

def MIPRE.Cost.Prog.tbCons : Prog

The step on a cons subtree: emit 1 and push the children.

Equations

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

def MIPRE.Cost.Prog.toBitsBody : Prog

The body of the serialization loop.

Equations

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

theorem MIPRE.Cost.Prog.toBitsBody_wellScoped : WellScoped 1 toBitsBody

theorem MIPRE.Cost.Prog.toBitsBody_stop (acc : BitStr) : Eval [(Data.list []).cons (encode acc)] toBitsBody (Data.nil.cons (encode acc)) (esize acc + 5)

theorem MIPRE.Cost.Prog.toBitsBody_step_nil (rest : List Data) (acc : BitStr) : Eval [(Data.list (Data.nil :: rest)).cons (encode acc)] toBitsBody ((Data.nil.cons Data.nil).cons ((Data.list rest).cons (encode (false :: acc)))) ((Data.list rest).size + esize acc + 12)

theorem MIPRE.Cost.Prog.toBitsBody_step_cons (a b : Data) (rest : List Data) (acc : BitStr) : Eval [(Data.list (a.cons b :: rest)).cons (encode acc)] toBitsBody ((Data.nil.cons Data.nil).cons ((Data.list (a :: b :: rest)).cons (encode (true :: acc)))) (a.size + b.size + (Data.list rest).size + esize acc + 18)

def MIPRE.Cost.Prog.toBitsInv (target : BitStr) (s : Data) : Prop

The invariant of the serialization loop for the target bits target: the state is cons stack acc with reverse acc ++ toBits stack₁ ++ … = target.

Equations

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

theorem MIPRE.Cost.Prog.toBitsLoop_runs (d : Data) (env : Env) (s : Data) (hs : toBitsInv d.toBits s) : ∃ t ≤ (s.stackMeasure + 1) * (8 * d.size + 21), ∃ (acc : BitStr), List.reverse acc = d.toBits ∧ Eval (s :: env) toBitsBody.loop (encode acc) t

def MIPRE.Cost.Prog.toBitsProg : Prog

The bits of a tree: toBitsProg on d computes encode d.toBits.

Equations

• MIPRE.Cost.Prog.toBitsProg = (((MIPRE.Cost.Prog.var 0).cons MIPRE.Cost.Prog.nil).cons MIPRE.Cost.Prog.nil).let_ (MIPRE.Cost.Prog.toBitsBody.loop.let_ MIPRE.Cost.Prog.revProg)

theorem MIPRE.Cost.Prog.toBitsProg_wellScoped : WellScoped 1 toBitsProg

theorem MIPRE.Cost.Prog.toBitsProg_runs (d : Data) : ∃ t ≤ (d.size + 2) * (13 * d.size + 41), toBitsProg.Runs d (encode d.toBits) t

noncomputable def MIPRE.Cost.PolyTimeFun.toBits : PolyTimeFun Data BitStr

The bits of a tree, in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.toBits_apply (d : Data) : toBits.toFun d = d.toBits