Finite witness-bound setup #
The bound interface has a concrete instance for the linear certificate bound
n + 1. It charges initialization, counter generation, and every visited work
or output cell. The certificate-storing compiler can consume the resulting
canonical unary counter without inspecting the external witness stream.
theorem
Complexity.WitnessBoundSetup.liftedSafety
{r : ℕ}
{bound : ℕ → ℕ}
(setup : WitnessBoundSetup r bound)
(x : List Bool)
:
setup.machine.liftLast.HoareSafety
(fun (inp : Tape) (work : Fin (r + 1 + 1) → Tape) (out : Tape) =>
fresh x inp (fun (i : Fin (r + 1)) => work i.castSucc) out)
fun (inp : Tape) (work : Fin (r + 1 + 1) → Tape) (out : Tape) =>
{ state := (), input := inp, work := fun (i : Fin (r + 1)) => work i.castSucc, output := out }.WithinDecisionSpace
x.length (setup.space x.length)
A bound-setup phase can run alongside an uncharged external witness tape without changing its ordinary all-prefix decision-space budget.
Realize the linear witness bound with one charged counter tape.
Both explicit resource budgets are 4 * n + 11.
Equations
- One or more equations did not get rendered due to their size.