Documentation

Complexitylib.Models.TuringMachine.Witness.BoundSetup.Reserved

Fresh tapes reserved alongside bound setup #

The setup uses private scratch. Separate future verifier, pair, and witness tapes start genuinely blank at head zero and become parked blank during the setup's first actual step. The extra tapes do not borrow the setup's private scratch contents and do not add a running-time charge.

source
def Complexity.WitnessBoundSetup.reservedReady {r : ℕ} (x : List Bool) (bound extra : ℕ) :
TapePred (r + 1 + extra)

Setup's canonical endpoint projected to its own block, with separately reserved tapes still blank and parked.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Complexity.WitnessBoundSetup.reservedReady_work {r : ℕ} (x : List Bool) (B extra : ℕ) {inp : Tape} {work : Fin (r + 1 + extra) → Tape} {out : Tape} (h : reservedReady x B extra inp work out) (i : Fin (r + 1 + extra)) :
    (work i).head = 1 ∧ (work i).StartInvariant

    Every reserved-setup work tape is parked and start-invariant, including both genuinely private setup scratch and separately reserved blank tapes.

    source
    theorem Complexity.WitnessBoundSetup.prepares_time_pos {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (x : List Bool) {c : Cfg (r + 1) setup.machine.Q} {t : ℕ} (hr : setup.machine.reachesIn t (setup.machine.initCfg x) c) (hready : ready x (bound x.length) c.input c.work c.output) :
    0 < t

    A completed setup run is nonempty because it parks the initially zero output head at cell one. This covers the initialization mismatch of liftCfg.

    source
    theorem Complexity.WitnessBoundSetup.prepares_reserved {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (extra : ℕ) (x : List Bool) :
    (setup.machine.liftTM extra).HoareTime (fresh x) (reservedReady x (bound x.length) extra) (setup.time x.length)

    An actual initialized setup run reserves fresh tapes without extra steps.

    source
    theorem Complexity.WitnessBoundSetup.safety_reserved {r : ℕ} {bound : ℕ → ℕ} (setup : WitnessBoundSetup r bound) (extra : ℕ) (x : List Bool) :
    (setup.machine.liftTM extra).HoareSafety (fresh x) fun (inp : Tape) (work : Fin (r + 1 + extra) → Tape) (out : Tape) => { state := (), input := inp, work := work, output := out }.WithinDecisionSpace x.length (max (setup.space x.length) 1)

    Reserving blank tapes costs at most the parked cell, independently of time.